coe_mul — Mathlib

English

The underlying function of the product of two continuous linear endomorphisms is the composition of their underlying functions: coe(f * g) = f ∘ g.

Русский

Функция, соответствующая произведению двух непрерывных линейных эндоморфизмов, равна композиции соответствующих функций: coe(f * g) = f ∘ g.

LaTeX

$$$ \text{coe}(f \cdot g) = f \circ g $$$

Lean4

@[simp]
theorem coe_mul (f g : M₁ →L[R₁] M₁) : ⇑(f * g) = f ∘ g :=
  rfl

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