instCoeOutLinearEquivId — Mathlib

English

For isometries g and f, the underlying linear map of their composition equals the composition of their linear maps.

Русский

Для изометрий g и f линейное отображение, лежащее в основе их композиции, равно композиции их линейных отображений.

LaTeX

$$$ (g \circ f)^{\mathrm{toLinearMap}} = g^{\mathrm{toLinearMap}} \circ f^{\mathrm{toLinearMap}} $$$

Lean4

instance : CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂) :=
  ⟨IsometryEquiv.toLinearEquiv⟩

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