gcd_eq_left_iff — Mathlib

English

In a GCDMonoid α, gcd((b·a),(c·a)) is associated with gcd(b,c)·a.

Русский

В GCD-монойде gcd(b·a, c·a) ассоциировано с gcd(b,c)·a.

LaTeX

$$$$ \text{Associated}(\gcd(b\cdot a, c\cdot a), \gcd(b,c) \cdot a) $$$$

Lean4

theorem gcd_eq_left_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) : gcd a b = a ↔ a ∣ b :=
  (Iff.intro fun eq => eq ▸ gcd_dvd_right _ _) fun hab =>
    dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) hab)

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