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.

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
theorem Tactic.NormNum.nat_gcd_helper_dvd_left (x : ) (y : ) (h : y % x = 0) :
Nat.gcd x y = x
theorem Tactic.NormNum.nat_gcd_helper_dvd_right (x : ) (y : ) (h : x % y = 0) :
Nat.gcd x 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) :
Nat.gcd x 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) :
Nat.gcd x y = d
theorem Tactic.NormNum.nat_gcd_helper_1' (x : ) (y : ) (a : ) (b : ) (h : y * b = x * a + 1) :
Nat.gcd x y = 1
theorem Tactic.NormNum.nat_gcd_helper_2' (x : ) (y : ) (a : ) (b : ) (h : x * a = y * b + 1) :
Nat.gcd x y = 1
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
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
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
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

      Evaluates the Int.gcd function.

      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