fact_prime_three

Mathlib.Data.PNat.Prime

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

English

The instance asserting that 3 is prime in ℕ+.

Русский

Экземпляр, доказывающий, что 3 простое в ℕ+.

LaTeX

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

Lean4

instance fact_prime_three : Fact (3 : ℕ+).Prime :=
  ⟨prime_three⟩

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

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

Разделы

Аффилиация

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