addCommMonoidWithOne

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Lean4

instance addCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (WithTop α) :=
  { WithTop.addMonoidWithOne, WithTop.addCommMonoid with }
    -- instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithTop α) where
    --   add_le_add_left _ _ := add_le_add_left
    --
    -- instance linearOrderedAddCommMonoidWithTop [LinearOrderedAddCommMonoid α] :
    --     LinearOrderedAddCommMonoidWithTop (WithTop α) :=
    --   { WithTop.orderTop, WithTop.linearOrder, WithTop.orderedAddCommMonoid with
    --     top_add' := WithTop.top_add }
    --

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

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

Разделы

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

Аффилиация

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