instFactPrimeValOfPrime

Mathlib.Data.PNat.Prime

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

English

For any p ∈ ℕ+, if p is prime, then p viewed as a natural is prime.

Русский

Пусть p ∈ ℕ+, если p простое, то p, как число в ℕ, является простым.

LaTeX

$$$ p \\Pr ime \\Rightarrow Nat.Prime p.val $$$

Lean4

instance {p : ℕ+} [h : Fact p.Prime] : Fact (p : ℕ).Prime :=
  h

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

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

Разделы

Аффилиация

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