Prime

Mathlib.Data.Num.Prime

URI: https://scilib.ai/kg/mathlib#PosNum.Prime

Lean4

/-- Primality predicate for a `PosNum`. -/
@[simp]
def Prime (n : PosNum) : Prop :=
  Nat.Prime n

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

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

Разделы

Аффилиация

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