instMul — Mathlib

English

The set of all continuous linear endomorphisms M1 →L[R1] M1 forms a monoid under composition, i.e., multiplication is given by composition: f * g = f ∘ g.

Русский

Множество всех непрерывных линейных эндоморфизмов M1 →L[R1] M1 образует моноид относительно операции композиции: f * g = f ∘ g.

LaTeX

$$$ f * g = f \circ g $$$

Lean4

instance instMul : Mul (M₁ →L[R₁] M₁) :=
  ⟨comp⟩

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