exists_prime_and_dvd

Mathlib.Data.Nat.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Nat.exists_prime_and_dvd

English

If n ≠ 1, there exists a prime p with p | n.

Русский

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

LaTeX

$$$\\\\forall n \\\\in \\\\mathbb{N}, n \\\\neq 1 \\\\Rightarrow \\\\exists p, \\\\mathrm{Prime}(p) \\\\land p \\\\mid n$$$

Lean4

theorem exists_prime_and_dvd {n : ℕ} (hn : n ≠ 1) : ∃ p, Prime p ∧ p ∣ n :=
  ⟨minFac n, minFac_prime hn, minFac_dvd _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru