fact_prime_five

Mathlib.Data.PNat.Prime

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

English

The instance asserting that 5 is prime in ℕ+.

Русский

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

LaTeX

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

Lean4

instance fact_prime_five : Fact (5 : ℕ+).Prime :=
  ⟨prime_five⟩

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

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

Разделы

Аффилиация

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