not_dvd_one

Mathlib.Data.Nat.Prime.Defs

URI: https://scilib.ai/kg/mathlib#Nat.Prime.not_dvd_one

English

If p is prime, then p does not divide 1.

Русский

Если p простое, то p не делит 1.

LaTeX

$$$\\\\forall p \\\\in \\\\mathbb{N}, \\\\mathrm{Prime}(p) \\\\rightarrow \\\\\\neg (p \\\\mid 1).$$$

Lean4

theorem not_dvd_one {p : ℕ} (pp : Prime p) : ¬p ∣ 1 :=
  Irreducible.not_dvd_one pp

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

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

Разделы

Аффилиация

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