addMonoidWithOne

Mathlib.Data.Num.ZNum

URI: https://scilib.ai/kg/mathlib#ZNum.addMonoidWithOne

Lean4

instance addMonoidWithOne : AddMonoidWithOne ZNum :=
  { ZNum.addMonoid with
    one := 1
    natCast := fun n => ZNum.ofInt' n
    natCast_zero := show (Num.ofNat' 0).toZNum = 0 by rw [Num.ofNat'_zero]; rfl
    natCast_succ := fun n =>
      show (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1 by
        rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one] }
    -- The next theorems are declared outside of the instance to prevent timeouts.

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

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

Разделы

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

Аффилиация

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