dvd_mul — Mathlib

English

Let p be a prime natural and m,n integers. If p divides m n in ℤ, then p divides m.natAbs or p divides n.natAbs.

Русский

Пусть p — простое число, m,n ∈ ℤ. Если p делит произведение m n в целых, то p делит |m| или p делит |n|.

LaTeX

$$$p\\text{ prime} \\land p \\mid mn \\implies p \\mid |m| \\lor p \\mid |n|.$$$

Lean4

theorem dvd_mul {m n : ℤ} {p : ℕ} (hp : Nat.Prime p) (h : (p : ℤ) ∣ m * n) : p ∣ m.natAbs ∨ p ∣ n.natAbs := by
  rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.natCast_dvd]

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