gcd_mul_lcm — Mathlib

English

For any a,b in Euclidean domain R, gcd(a,b) = a·gcdA(a,b) + b·gcdB(a,b).

Русский

Для любых a,b в евклидовой области R gcd(a,b) = a·gcdA(a,b) + b·gcdB(a,b).

LaTeX

$$$\\gcd(a,b) = a \\cdot gcdA(a,b) + b \\cdot gcdB(a,b)$$$

Lean4

@[simp]
theorem gcd_mul_lcm (x y : R) : gcd x y * lcm x y = x * y :=
  by
  rw [lcm]; by_cases h : gcd x y = 0
  · rw [h, zero_mul]
    rw [EuclideanDomain.gcd_eq_zero_iff] at h
    rw [h.1, zero_mul]
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  generalize gcd x y = g at h hr ⊢; subst hr
  rw [mul_assoc, mul_div_cancel_left₀ _ h]

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