# 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.

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
theorem Tactic.NormNum.nat_gcd_helper_dvd_left (x : ) (y : ) (h : y % x = 0) :
x.gcd y = x
theorem Tactic.NormNum.nat_gcd_helper_dvd_right (x : ) (y : ) (h : x % y = 0) :
x.gcd y = y
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
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
theorem Tactic.NormNum.nat_gcd_helper_1' (x : ) (y : ) (a : ) (b : ) (h : y * b = x * a + 1) :
x.gcd y = 1
theorem Tactic.NormNum.nat_gcd_helper_2' (x : ) (y : ) (a : ) (b : ) (h : x * a = y * b + 1) :
x.gcd y = 1
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
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
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
theorem Tactic.NormNum.isNat_gcd {x : } {y : } {nx : } {ny : } {z : } :
nx.gcd ny = zMathlib.Meta.NormNum.IsNat (x.gcd y) z
theorem Tactic.NormNum.isNat_lcm {x : } {y : } {nx : } {ny : } {z : } :
nx.lcm ny = zMathlib.Meta.NormNum.IsNat (x.lcm y) z
theorem Tactic.NormNum.isInt_gcd {x : } {y : } {nx : } {ny : } {z : } :
nx.gcd ny = zMathlib.Meta.NormNum.IsNat (x.gcd y) z
theorem Tactic.NormNum.isInt_lcm {x : } {y : } {nx : } {ny : } {z : } :
nx.lcm ny = zMathlib.Meta.NormNum.IsNat (x.lcm y) z
def Tactic.NormNum.proveNatGCD (ex : Q()) (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 Equations • One or more equations did not get rendered due to their size. Instances For def Tactic.NormNum.proveNatLCM (ex : Q()) (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
• One or more equations did not get rendered due to their size.
Instances For

Evaluates the Nat.lcm function.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Tactic.NormNum.proveIntGCD (ex : Q()) (ey : Q()) :
(ed : Q()) × Q(«$ex».gcd «$ey» = «$ed») Given two integers, return their GCD and an equality proof. Panics if ex or ey aren't integer literals. Equations • One or more equations did not get rendered due to their size. Instances For Evaluates the Int.gcd function. Equations • One or more equations did not get rendered due to their size. Instances For def Tactic.NormNum.proveIntLCM (ex : Q()) (ey : Q()) : (ed : Q()) × Q(«$ex».lcm «$ey» = «$ed»)

Given two integers, return their LCM and an equality proof. Panics if ex or ey aren't integer literals.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Evaluates the Int.lcm function.

Equations
• One or more equations did not get rendered due to their size.
Instances For