Def endVecRingEquivMatrixEnd

Modification history

2024-11-08 13:01
Mathlib/LinearAlgebra/Matrix/ToLin.lean
feat(LinearAlgebra/Matrix/ToLin): for R-module M, End(Mⁿ) ≅ Matₙₓₙ(End(M)) (#18752) …
Added endVecRingEquivMatrixEndView on Github →