exists_prime_and_dvd — Mathlib

English

For any integer n with |n| ≠ 1, there exists a prime p such that p divides n.

Русский

Для целого n с |n| ≠ 1 существует простое число p, делящее n.

LaTeX

$$$\\forall n \\in \\mathbb{Z},\\ |n| \\neq 1 \\Rightarrow \\exists p, \\text{Prime}(p) \\land p \\mid n$.$$

Lean4

theorem exists_prime_and_dvd {n : ℤ} (hn : n.natAbs ≠ 1) : ∃ p, Prime p ∧ p ∣ n :=
  by
  obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn
  exact ⟨p, Nat.prime_iff_prime_int.mp pp, Int.natCast_dvd.mpr pd⟩

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