toLinearMap_comp — Mathlib

English

The linear map underlying the composition of two isometries equals the composition of their underlying linear maps.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toLinearMap_comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : (g.comp f).toLinearMap = g.toLinearMap.comp f.toLinearMap :=
  rfl

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