Documentation

Mathlib.Tactic.NormNum.GCD

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) :
Int.gcd x y = d
source
theorem Tactic.NormNum.nat_gcd_helper_dvd_left (x : ℕ) (y : ℕ) (h : y % x = 0) :
Nat.gcd x y = x
source
theorem Tactic.NormNum.nat_gcd_helper_dvd_right (x : ℕ) (y : ℕ) (h : x % y = 0) :
Nat.gcd x 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) :
Nat.gcd x 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) :
Nat.gcd x y = d
source
theorem Tactic.NormNum.nat_gcd_helper_1' (x : ℕ) (y : ℕ) (a : ℕ) (b : ℕ) (h : y * b = x * a + 1) :
Nat.gcd x y = 1
source
theorem Tactic.NormNum.nat_gcd_helper_2' (x : ℕ) (y : ℕ) (a : ℕ) (b : ℕ) (h : x * a = y * b + 1) :
Nat.gcd x y = 1
source
theorem Tactic.NormNum.nat_lcm_helper (x : ℕ) (y : ℕ) (d : ℕ) (m : ℕ) (hd : Nat.gcd x y = d) (d0 : Nat.beq d 0 = false) (dm : x * y = d * m) :
Nat.lcm x y = m
source
theorem Tactic.NormNum.int_gcd_helper {x : ℤ} {y : ℤ} {x' : ℕ} {y' : ℕ} {d : ℕ} (hx : Int.natAbs x = x') (hy : Int.natAbs y = y') (h : Nat.gcd x' y' = d) :
Int.gcd x y = d
source
theorem Tactic.NormNum.int_lcm_helper {x : ℤ} {y : ℤ} {x' : ℕ} {y' : ℕ} {d : ℕ} (hx : Int.natAbs x = x') (hy : Int.natAbs y = y') (h : Nat.lcm x' y' = d) :
Int.lcm x 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 → Nat.gcd nx ny = z → Mathlib.Meta.NormNum.IsNat (Nat.gcd x 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 → Nat.lcm nx ny = z → Mathlib.Meta.NormNum.IsNat (Nat.lcm x 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 → Int.gcd nx ny = z → Mathlib.Meta.NormNum.IsNat (Int.gcd x 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 → Int.lcm nx ny = z → Mathlib.Meta.NormNum.IsNat (Int.lcm x y) z
source
def Tactic.NormNum.evalNatGCD :
Mathlib.Meta.NormNum.NormNumExt
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.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.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