Invertible_Matrix_to_Automorphism

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Invertible_Matrix_to_Automorphism is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Let $R$ be a ring with unity. Let $n \in \Z_{>0}$ be a (strictly) positive integer. Let $G$ be an $n$-dimensional $R$-module. Let $\map {\mathcal M_R} n$ be the $n \times n$ matrix space over $R$. Let $\map {\mathcal L_R} G$ be the set of all linear operators on $G$. Then the invertible elements of the ring of square matrices $\struct {\map {\mathcal M_R} n, +, \times}$ correspond directly to automorphisms of $\map {\mathcal L_R} G$.

Why this node was retired

The posted statement is

theorem Invertible_Matrix_to_Automorphism {R : Type _} [CommRing R] (n : ℕ) (A : Matrix (Fin n) (Fin n) R) (hA : IsUnit A) : ∃ (phi : (Fin n → R) ≃ₗ[R] (Fin n → R)), True := by sorry

The goal is ∃ (phi : (Fin n → R) ≃ₗ[R] (Fin n → R)), True, witnessed by the identity map, with no link to A. The invertibility hypothesis hA is never used.

What a faithful statement would require

The conclusion must identify phi with the linear map determined by A.

No corrected replacement node exists yet.