gcd_dvd — Mathlib

English

For any a,b in a Euclidean domain, gcd(a,b) divides a and gcd(a,b) divides b.

Русский

Для любых a,b в евклидовом кольце, gcd(a,b) делит и a, и b.

LaTeX

$$$ gcd\,a\,b \mid a \land gcd\,a\,b \mid b $$$

Lean4

theorem gcd_dvd (a b : R) : gcd a b ∣ a ∧ gcd a b ∣ b :=
  GCD.induction a b
    (fun b => by
      rw [gcd_zero_left]
      exact ⟨dvd_zero _, dvd_rfl⟩)
    fun a b _ ⟨IH₁, IH₂⟩ => by
    rw [gcd_val]
    exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩

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