English
If P is an invertible n×n matrix over a ring R, then left-multiplication by P yields a linear equivalence on the free module R^n, i.e., a linear isomorphism φ_P: R^n → R^n given by x ↦ P x.
Русский
Если P — обратимая матрица размером n×n над кольцом R, то умножение слева на P даёт линейное биекция R^n → R^n, то есть линейное изоморфизм φ_P: R^n → R^n, задаваемый x ↦ Px.
LaTeX
$$$P \\in GL_n(R) \\Rightarrow (x \\mapsto P x): R^n \\to R^n \\text{ is a linear isomorphism}$$$
Lean4
/-- An invertible matrix yields a linear equivalence from the free module to itself.
See `Matrix.toLinearEquiv` for the same map on arbitrary modules.
-/
def toLinearEquiv' (P : Matrix n n R) (_ : Invertible P) : (n → R) ≃ₗ[R] n → R :=
GeneralLinearGroup.generalLinearEquiv _ _ <| Matrix.GeneralLinearGroup.toLin <| unitOfInvertible P
