gcd_eq_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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