instGCDMonoid — Mathlib

English

For every k ∈ ℤ, k is associated to k.natAbs.

Русский

Для каждого k ∈ ℤ элемент k ассоциирован с k.natAbs.

LaTeX

$$∀ k ∈ ℤ, \operatorname{Associated}(k, k.natAbs)$$

Lean4

instance : GCDMonoid ℤ where
  gcd a b := Int.gcd a b
  lcm a b := Int.lcm a b
  gcd_dvd_left := Int.gcd_dvd_left
  gcd_dvd_right := Int.gcd_dvd_right
  dvd_gcd := dvd_coe_gcd
  gcd_mul_lcm a
    b := by
    rw [← Int.natCast_mul, gcd_mul_lcm, ← natAbs_mul, natCast_natAbs, abs_eq_normalize]
    exact normalize_associated (a * b)
  lcm_zero_left _ := natCast_eq_zero.2 <| Nat.lcm_zero_left _
  lcm_zero_right _ := natCast_eq_zero.2 <| Nat.lcm_zero_right _

Похожие утверждения