lcm_eq_right_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lcm_eq_right_iff [NormalizedGCDMonoid α] (a b : α) (h : normalize b = b) : lcm a b = b ↔ a ∣ b := by
  simpa only [lcm_comm b a] using lcm_eq_left_iff b a h

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