coe_mul — Mathlib

English

There is a monoid structure on endomorphisms given by composition, with identity as the unit.

Русский

Существует моноидальная структура на концевых отображениях, заданная композициями, с единицей как нейтральным элементом.

LaTeX

$$instance instMonoid : Monoid (E →ₗᵢ[R] E) where one := id mul := comp mul_assoc := comp_assoc one_mul := id_comp mul_one := comp_id$$

Lean4

@[simp]
theorem coe_mul (f g : E →ₗᵢ[R] E) : ⇑(f * g) = f ∘ g :=
  rfl

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