coe_toLinearMap_mul — Mathlib

English

The linear map corresponding to the product of two linear equivalences is the product of their linear maps, i.e., composition.

Русский

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

LaTeX

$$$ (↑(e_1 \cdot e_2) : M \to M) = (↑e_1 : M \to M) \circ (↑e_2 : M \to M) $$$

Lean4

@[simp]
theorem coe_toLinearMap_mul {e₁ e₂ : M ≃ₗ[R] M} : (↑(e₁ * e₂) : M →ₗ[R] M) = (e₁ : M →ₗ[R] M) * (e₂ : M →ₗ[R] M) :=
  rfl

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