`norm_num` extensions for GCD-adjacent functions #

This module defines some norm_num extensions for functions such as Nat.gcd, Nat.lcm, Int.gcd, and Int.lcm.

Note that Nat.coprime is reducible and defined in terms of Nat.gcd, so the Nat.gcd extension also indirectly provides a Nat.coprime extension.

source

theorem Tactic.NormNum.int_gcd_helper' {d : ℕ} {x y : ℤ} (a b : ℤ) (h₁ : ↑d ∣ x) (h₂ : ↑d ∣ y) (h₃ : x * a + y * b = ↑d) :

x.gcd y = d

source

theorem Tactic.NormNum.nat_gcd_helper_dvd_left (x y : ℕ) (h : y % x = 0) :

x.gcd y = x

source

theorem Tactic.NormNum.nat_gcd_helper_dvd_right (x y : ℕ) (h : x % y = 0) :

x.gcd y = y

source

theorem Tactic.NormNum.nat_gcd_helper_2 (d x y a b : ℕ) (hu : x % d = 0) (hv : y % d = 0) (h : x * a = y * b + d) :

x.gcd y = d

source

theorem Tactic.NormNum.nat_gcd_helper_1 (d x y a b : ℕ) (hu : x % d = 0) (hv : y % d = 0) (h : y * b = x * a + d) :

x.gcd y = d

source

theorem Tactic.NormNum.nat_gcd_helper_1' (x y a b : ℕ) (h : y * b = x * a + 1) :

x.gcd y = 1

source

theorem Tactic.NormNum.nat_gcd_helper_2' (x y a b : ℕ) (h : x * a = y * b + 1) :

x.gcd y = 1

source

theorem Tactic.NormNum.nat_lcm_helper (x y d m : ℕ) (hd : x.gcd y = d) (d0 : d.beq 0 = false) (dm : x * y = d * m) :

x.lcm y = m

source

theorem Tactic.NormNum.int_gcd_helper {x y : ℤ} {x' y' d : ℕ} (hx : x.natAbs = x') (hy : y.natAbs = y') (h : x'.gcd y' = d) :

x.gcd y = d

source

theorem Tactic.NormNum.int_lcm_helper {x y : ℤ} {x' y' d : ℕ} (hx : x.natAbs = x') (hy : y.natAbs = y') (h : x'.lcm y' = d) :

x.lcm y = d

source

theorem Tactic.NormNum.isNat_gcd {x y nx ny z : ℕ} :

Mathlib.Meta.NormNum.IsNat x nx → Mathlib.Meta.NormNum.IsNat y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z

source

theorem Tactic.NormNum.isNat_lcm {x y nx ny z : ℕ} :

Mathlib.Meta.NormNum.IsNat x nx → Mathlib.Meta.NormNum.IsNat y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z

source

theorem Tactic.NormNum.isInt_gcd {x y nx ny : ℤ} {z : ℕ} :

Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z

source

theorem Tactic.NormNum.isInt_lcm {x y nx ny : ℤ} {z : ℕ} :

Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z

source

def Tactic.NormNum.proveNatGCD (ex ey : Q(ℕ)) :

(ed : Q(ℕ)) × Q(«$ex».gcd «$ey» = «$ed»)

Given natural number literals ex and ey, return their GCD as a natural number literal and an equality proof. Panics if ex or ey aren't natural number literals.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Tactic.NormNum.evalNatGCD :

Mathlib.Meta.NormNum.NormNumExt

Evaluate the Nat.gcd function.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Tactic.NormNum.proveNatLCM (ex ey : Q(ℕ)) :

(ed : Q(ℕ)) × Q(«$ex».lcm «$ey» = «$ed»)

Given natural number literals ex and ey, return their LCM as a natural number literal and an equality proof. Panics if ex or ey aren't natural number literals.

Equations