Theorem Matrix.toRingEquiv_reindexStarAlgEquiv

Modification history

2026-11-10 20:16

Mathlib/LinearAlgebra/Matrix/Reindex.lean

feat(LinearAlgebra/Matrix/Reindex): add `Matrix.reindexStarAlgEquiv` (#45199) …

Added Matrix.toRingEquiv_reindexStarAlgEquiv View on Github →