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

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

Instances For

source
def Tactic.NormNum.evalNatLCM :
Mathlib.Meta.NormNum.NormNumExt

Evaluates the `Nat.lcm` function.

Equations

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

Instances For

source
def Tactic.NormNum.proveIntGCD (ex 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

source
def Tactic.NormNum.evalIntGCD :
Mathlib.Meta.NormNum.NormNumExt

Evaluates the `Int.gcd` function.

Equations

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

Instances For

source
def Tactic.NormNum.proveIntLCM (ex 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

source
def Tactic.NormNum.evalIntLCM :
Mathlib.Meta.NormNum.NormNumExt

Evaluates the `Int.lcm` function.

Equations

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

Instances For

source
theorem Tactic.NormNum.isInt_ratNum {q : ℚ} {n : ℤ} {n' d : ℕ} :
Mathlib.Meta.NormNum.IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → Mathlib.Meta.NormNum.IsInt q.num n
source
theorem Tactic.NormNum.isNat_ratDen {q : ℚ} {n : ℤ} {n' d : ℕ} :
Mathlib.Meta.NormNum.IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → Mathlib.Meta.NormNum.IsNat q.den d
source
def Tactic.NormNum.evalRatNum :
Mathlib.Meta.NormNum.NormNumExt

Evaluates the `Rat.num` function.

Equations

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

Instances For

source
def Tactic.NormNum.evalRatDen :
Mathlib.Meta.NormNum.NormNumExt

Evaluates the `Rat.den` function.

Equations

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

Instances For