English
Let R be a commutative semiring and M a square matrix of size n with entries in R. Then M is invertible as a matrix if and only if the associated linear map M.toLin' : R^n → R^n is invertible, i.e. an automorphism.
Русский
Пусть R — коммутативное полукольцо, а M — квадратная матрица размера n над R. Тогда M обратима как матрица тогда и только тогда, когда соответствующее линейное отображение M.toLin' : R^n → R^n обратимо, то есть является изоморфизмом.
LaTeX
$$$\\operatorname{IsUnit}(M^{\\mathrm{toLin}'}) \\;\\iff\\; \\operatorname{IsUnit}(M) ,\\quad M \\in \\mathrm{Mat}_{n}(R).$$$
Lean4
@[simp]
theorem isUnit_toLin'_iff {M : Matrix n n R} : IsUnit M.toLin' ↔ IsUnit M :=
isUnit_map_iff LinearMap.toMatrixAlgEquiv'.symm M
