toLinAlgEquiv_mul — Mathlib

English

The matrix–linear equivalence that sends matrices to linear endomorphisms respects multiplication: the equivalence of A B equals the composition of the corresponding linear maps.

Русский

Матрично‑линейное эквивалентное отображение сохраняет умножение: матрица A B соответствует композиции соответствующих линейных отображений.

LaTeX

$$$\operatorname{toLinAlgEquiv}_{v_1}(A B) = (\operatorname{toLinAlgEquiv}_{v_1} A) \circ (\operatorname{toLinAlgEquiv}_{v_1} B).$$$

Lean4

theorem toLinAlgEquiv_mul (A B : Matrix n n R) :
    Matrix.toLinAlgEquiv v₁ (A * B) = (Matrix.toLinAlgEquiv v₁ A).comp (Matrix.toLinAlgEquiv v₁ B) := by
  convert Matrix.toLin_mul v₁ v₁ v₁ A B

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