English
Let b1 and b2 be bases and M a matrix with entries in N₂. If we view M as a linear map via Matrix.toLinearMap₂ and then convert back to a matrix via toMatrix₂, we get back the original matrix M. In other words, these two coordinate transformations are inverses on matrices.
Русский
Пусть b1 и b2 — базисы, а M — матрица над полем N₂. Если матрицу M рассмотреть как линейное отображение через Matrix.toLinearMap₂ и затем вернуть её в виде матрицы через toMatrix₂, то получится исходная матрица M. Другими словами, эти преобразования взаимно обратны на матрицах.
LaTeX
$$$$ \operatorname{toMatrix}_{b_1,b_2}\bigl(\operatorname{toLinearMap}_{b_1,b_2}(M)\bigr) = M. $$$$
Lean4
@[simp]
theorem toMatrix₂_toLinearMap₂ (M : Matrix n m N₂) : LinearMap.toMatrix₂ b₁ b₂ (Matrix.toLinearMap₂ b₁ b₂ M) = M :=
(LinearMap.toMatrix₂ b₁ b₂).apply_symm_apply M
