Let R be a ring with unity whose zero is 0R and whose unity is 1R. Let n∈Z>0 be a (strictly) positive integer. Let \struct\map\MMRn,+,× denote the ring of square matrices of order n over R. The unit matrix over RIn=1R0R0R⋮0R0R1R0R⋮0R0R0R1R⋮0R⋯⋯⋯⋱⋯0R0R0R⋮1R is the identity element of \struct\map\MMRn,+,×.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Unit_Matrix_is_Unity_of_Ring_of_Square_Matrices {R : Type _} [Ring R] (n : ℕ) (A : Matrix (Fin n) (Fin n) R) : (1 : Matrix (Fin n) (Fin n) R) * A = A ∧ A * (1 : Matrix (Fin n) (Fin n) R) = A := by sorry