isOne

Mathlib.Data.Num.Basic

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

Lean4

/-- Returns a Boolean for whether the `PosNum` is `one`. -/
def isOne : PosNum → Bool
  | 1 => true
  | _ => false

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

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

Разделы

Аффилиация

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