withBotMap — Mathlib

Lean4
/-- A version of `WithBot.map` for `AddMonoidHom`s. -/
@[simps -fullyApplied]
protected def _root_.AddMonoidHom.withBotMap {M N : Type*} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :
    WithBot M →+ WithBot N :=
  { ZeroHom.withBotMap f.toZeroHom, AddHom.withBotMap f.toAddHom with toFun := WithBot.map f }
    -- instance orderedAddCommMonoid [OrderedAddCommMonoid α] : OrderedAddCommMonoid (WithBot α) :=
    --   { WithBot.partialOrder, WithBot.addCommMonoid with
    --     add_le_add_left := fun _ _ h c => add_le_add_left h c }
    --
    -- instance linearOrderedAddCommMonoid [LinearOrderedAddCommMonoid α] :
    --     LinearOrderedAddCommMonoid (WithBot α) :=
    --   { WithBot.linearOrder, WithBot.orderedAddCommMonoid with }
Похожие утверждения