prime_two

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#PNat.prime_two

English

The element 2 is prime in the positive naturals.

Русский

Элемент 2 является простым в ℕ+.

LaTeX

$$$ 2 \\\\text{ is prime}$$$

Lean4

theorem prime_two : (2 : ℕ+).Prime :=
  Nat.prime_two

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

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

Разделы

Аффилиация

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