Theorem Matrix.toRingEquiv_prodAlgEquiv

Modification history

2026-11-10 14:51
Mathlib/Data/Matrix/Basic.lean
feat(LinearAlgebra/Matrix): add the `prodEquiv` for `Matrix`, `GL` and `SL` (#44876)
Added Matrix.toRingEquiv_prodAlgEquivView on Github →