instMulOfIsOrderedMonoid — Mathlib

English

If f: γ →*o δ, g: β →*o γ, h: α →*o β, then (f.comp g).comp h = f.comp (g.comp h).

Русский

Если f: γ →*o δ, g: β →*o γ и h: α →*o β, тогда (f.comp g).comp h = f.comp (g.comp h).

LaTeX

$$$ (f.comp g).comp h = f.comp (g.comp h) $$$

Lean4

/-- For two ordered monoid morphisms `f` and `g`, their product is the ordered monoid morphism
sending `a` to `f a * g a`. -/
@[to_additive /-- For two ordered additive monoid morphisms `f` and `g`, their product is the
    ordered additive monoid morphism sending `a` to `f a + g a`. -/
    ]
instance [IsOrderedMonoid β] : Mul (α →*o β) :=
  ⟨fun f g => { (f * g : α →* β) with monotone' := f.monotone'.mul' g.monotone' }⟩

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