instMul — Mathlib

English

The underlying monoid-with-zero homomorphism of f equals the coerced representation of f.

Русский

Базовый моноид с нулём-гомоморфизм f равен приведённому представлению f.

LaTeX

$$$f.toMonoidWithZeroHom = f$ (as MonoidWithZeroHom)$$

Lean4

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

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