Commit 2026-11-10 20:16 96ddf2ec

View on Github →

feat(LinearAlgebra/Matrix/Reindex): add Matrix.reindexStarAlgEquiv (#45199) This code was suggested by @j-loreaux in his review of #41847. It adds Matrix.reindexStarAlgEquiv, a relabeling the rows and columns of a square matrix as a star-algebra equivalence. Its simp lemmas are next to the existing reindexAlgEquiv. This is the split that a previous reviewer asked for.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Defs.lean

Modified Mathlib/LinearAlgebra/Matrix/Reindex.lean

added theorem Matrix.coe_reindexStarAlgEquiv

added def Matrix.reindexStarAlgEquiv

added theorem Matrix.reindexStarAlgEquiv_refl

added theorem Matrix.reindexStarAlgEquiv_trans_reindexStarAlgEquiv

added theorem Matrix.symm_reindexStarAlgEquiv

added theorem Matrix.toAddEquiv_reindexStarAlgEquiv

added theorem Matrix.toAlgEquiv_reindexStarAlgEquiv

added theorem Matrix.toEquiv_reindexStarAlgEquiv

added theorem Matrix.toRingEquiv_reindexStarAlgEquiv