dvd_mul — Mathlib

English

For prime p, p divides mn if and only if p divides m or p divides n.

Русский

Для простого p верно: p делит произведение mn тогда и только тогда, когда p делит m или p делит n.

LaTeX

$$$\\\\forall p,m,n \\\\in \\\\mathbb{N}, \\\\mathrm{Prime}(p) \\\\rightarrow (p \\\\mid m n) \\\\Leftrightarrow (p \\\\mid m \\\\lor p \\\\mid n)$$$

Lean4

theorem dvd_mul {p m n : ℕ} (pp : Prime p) : p ∣ m * n ↔ p ∣ m ∨ p ∣ n :=
  ⟨fun H => or_iff_not_imp_left.2 fun h => (pp.coprime_iff_not_dvd.2 h).dvd_of_dvd_mul_left H,
    Or.rec (fun h : p ∣ m => h.mul_right _) fun h : p ∣ n => h.mul_left _⟩

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