monoidWithZero — Mathlib

English

Multiplication on the endomorphism set is associative: (f * g) * h = f * (g * h).

Русский

Умножение в множестве эндоморфизмов ассоциативно: (f * g) * h = f * (g * h).

LaTeX

$$$ (f * g) * h = f * (g * h) $$$

Lean4

instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁)
    where
  mul_zero f := ext fun _ => map_zero f
  zero_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  one_mul _ := ext fun _ => rfl
  mul_assoc _ _ _ := ext fun _ => rfl

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