gcd_eq_left — Mathlib

English

If m and n are associated, then for every k we have gcd(m,k) = gcd(n,k).

Русский

Если m ассоциировано с n, то для любого k выполняется gcd(m,k) = gcd(n,k).

LaTeX

$$$\\forall k : \\alpha, \\text{Associated}(m,n) \\Rightarrow \\gcd m k = \\gcd n k$$$

Lean4

theorem gcd_eq_left [NormalizedGCDMonoid α] {m n : α} (h : Associated m n) (k : α) : gcd m k = gcd n k :=
  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) (gcd_dvd_gcd h.dvd dvd_rfl)
    (gcd_dvd_gcd h.symm.dvd dvd_rfl)

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