fact_prime_two

Mathlib.Data.PNat.Prime

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

English

The instance asserting that 2 is prime in ℕ+.

Русский

Существование экземпляра, доказывающее, что 2 простое в ℕ+.

LaTeX

$$$ \\text{Fact}(2:\\mathbb{N}^+).Prime$$$

Lean4

instance fact_prime_two : Fact (2 : ℕ+).Prime :=
  ⟨prime_two⟩

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

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

Разделы

Аффилиация

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