addMonoidWithOne

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Lean4

instance addMonoidWithOne : AddMonoidWithOne (WithTop α) :=
  { WithTop.one, WithTop.addMonoid with natCast := fun n => ↑(n : α),
    natCast_zero := by simp only [Nat.cast_zero, WithTop.coe_zero],
    natCast_succ := fun n => by simp only [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one] }

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

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

Разделы

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

Аффилиация

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