lcm_eq_left_iff — Mathlib

English

For a NormalizedGCDMonoid α, lcm(a,b) = a iff b ∣ a, given h: normalize a = a.

Русский

В нормализованном gcd-монойде lcm(a,b) = a если и только если b ∣ a, при условии normalize(a)=a.

LaTeX

$$$ \operatorname{lcm}(a,b) = a \iff b \mid a $$$

Lean4

theorem lcm_eq_left_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize a = a) : lcm a b = a ↔ b ∣ a :=
  (Iff.intro fun eq => eq ▸ dvd_lcm_right _ _) fun hab =>
    dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) (dvd_lcm_left _ _)

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