dvd_or_dvd_of_dvd_lcm — Mathlib

English

If p is a prime and p divides the least common multiple of a and b, then p divides a or p divides b.

Русский

Если p — простое и p делит наименьшее общее кратное a и b, то p делит a или p делит b.

LaTeX

$$$$p \text{ prime} \wedge p \mid \mathrm{lcm}(a,b) \implies p \mid a \ or\ 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))

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