dvd_lcm — Mathlib

English

For a prime p, p | lcm a b iff p | a or p | b.

Русский

Для простого p: p делит НОК(a,b) тогда и только тогда, когда p делит a или p делит b.

LaTeX

$$$\forall {p,a,b : \mathbb{N}}, \text{Prime}(p) \Rightarrow \left(p \mid \operatorname{lcm}(a,b) \leftrightarrow (p \mid a \lor p \mid b)\right)$$$

Lean4

theorem dvd_lcm : p ∣ lcm a b ↔ p ∣ a ∨ p ∣ b :=
  ⟨hp.dvd_or_dvd_of_dvd_lcm, (Or.elim · (dvd_lcm_of_dvd_left · _) (dvd_lcm_of_dvd_right · _))⟩

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