English
If M and M' are inverse matrices (MM' = 1 and M'M = 1) with respect to bases v1,v2, then Matrix.toLin v1 v2 M and Matrix.toLin v2 v1 M' are inverse linear maps; they form a linear equivalence between M1 and M2.
Русский
Если M и M' — обратные друг другу матрицы (MM' = 1 и M' M = 1) относительно базисов v1,v2, то линейные отображения Matrix.toLin v1 v2 M и Matrix.toLin v2 v1 M' являются обратными друг другу и задают линейное биективное отображение между M1 и M2.
LaTeX
$$$MM' = 1 \text{ and } M' M = 1 \implies M_1 \cong_R M_2 ext{ with } \mathrm{toLin}_{v_1,v_2}(M) \text{ and } \mathrm{toLin}_{v_2,v_1}(M') \text{ as inverse}.$$$
Lean4
/-- Shortcut lemma for `Matrix.toLin_mul` and `LinearMap.comp_apply`. -/
theorem toLin_mul_apply [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) (x) :
Matrix.toLin v₁ v₃ (A * B) x = (Matrix.toLin v₂ v₃ A) (Matrix.toLin v₁ v₂ B x) := by
rw [Matrix.toLin_mul v₁ v₂, LinearMap.comp_apply]
