ofZNum'

Mathlib.Data.Num.Basic

URI: https://scilib.ai/kg/mathlib#Num.ofZNum'

Lean4

/-- Converts a `ZNum` to an `Option Num`, where `ofZNum' p = none` if `p < 0`. -/
def ofZNum' : ZNum → Option Num
  | 0 => some 0
  | ZNum.pos p => some (pos p)
  | ZNum.neg _ => none

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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