lcm_eq_zero_iff — Mathlib

English

In a gcd monoid, lcm(a,b) = 0 if and only if a = 0 or b = 0.

Русский

В gcd-монойде lcm(a,b) = 0 тогда, если и только если a = 0 или b = 0.

LaTeX

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

Lean4

@[simp]
theorem lcm_eq_zero_iff [GCDMonoid α] (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0 :=
  Iff.intro
    (fun h : lcm a b = 0 =>
      by
      have : Associated (a * b) 0 := (gcd_mul_lcm a b).symm.trans <| by rw [h, mul_zero]
      rwa [← mul_eq_zero, ← associated_zero_iff_eq_zero])
    (by rintro (rfl | rfl) <;> [apply lcm_zero_left; apply lcm_zero_right])

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