comp_symm — Mathlib

English

The action of the transitive composition on an element is the successive application of the middle maps.

Русский

Действие транспитивной композиции на элемент — это последовательное применение средних отображений.

LaTeX

$$$(e_{12} \\text{.trans} e_{23})\\; c = e_{23}(e_{12}(c))$$$

Lean4

theorem comp_symm : e.toLinearMap ∘ₛₗ e.symm.toLinearMap = LinearMap.id :=
  LinearMap.ext e.apply_symm_apply

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