dvd_or_dvd_of_dvd_lcm — Mathlib

English

For a prime p, p divides lcm(a,b) iff p divides a or p divides b.

Русский

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

LaTeX

$$$\forall {p,a,b} \in \mathbb{N}, \text{Prime}(p) \Rightarrow (p \mid \operatorname{lcm}(a,b) \iff p \mid a \lor p \mid b)$$$

Lean4

theorem dvd_or_dvd_of_dvd_lcm (h : p ∣ lcm a b) : p ∣ a ∨ p ∣ b :=
  dvd_or_dvd hp (h.trans (lcm_dvd_mul a b))

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