ne_one

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.Prime.ne_one

English

Every prime p in ℕ+ satisfies p ≠ 1.

Русский

Каждое простое число p в ℕ+ не равно 1.

LaTeX

$$$ \\text{for all } p, \\; p\\text{ prime } \\Rightarrow p \\neq 1$$$

Lean4

theorem ne_one {p : ℕ+} : p.Prime → p ≠ 1 := by
  intro pp contra
  apply Nat.Prime.ne_one pp
  rw [PNat.coe_eq_one_iff]
  apply contra

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

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

Разделы

Аффилиация

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