instMonoidWithZero

Mathlib.Algebra.Order.Ring.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.instMonoidWithZero

Lean4

instance instMonoidWithZero : MonoidWithZero (WithTop α)
    where
  __ := instMulZeroOneClass
  __ := instSemigroupWithZero
  npow n
    a :=
    match a, n with
    | (a : α), n => ↑(a ^ n)
    | ⊤, 0 => 1
    | ⊤, _n + 1 => ⊤
  npow_zero a := by cases a <;> simp
  npow_succ n a := by cases n <;> cases a <;> simp [pow_succ]

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

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

Разделы

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

Аффилиация

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