Commit 2026-06-06 21:53 5b9fcab5

View on Github →

feat(LinearAlgebra/Matrix): reindex as AddEquiv and RingEquiv (#39106) We had Matrix.reindex bundled as a LinearEquiv and an AlgEquiv, and this bundles it as an AddEquiv and a RingEquiv.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/Reindex.lean

added theorem Matrix.coe_reindexAddEquiv

added theorem Matrix.coe_reindexAlgEquiv

added theorem Matrix.coe_reindexLinearEquiv

added theorem Matrix.coe_reindexRingEquiv

added def Matrix.reindexAddEquiv

added theorem Matrix.reindexAddEquiv_refl_refl

added theorem Matrix.reindexAddEquiv_trans_reindexAddEquiv

deleted theorem Matrix.reindexAlgEquiv_symm

added theorem Matrix.reindexAlgEquiv_trans_reindexAlgEquiv

deleted theorem Matrix.reindexLinearEquiv_symm

deleted theorem Matrix.reindexLinearEquiv_trans

added theorem Matrix.reindexLinearEquiv_trans_reindexLinearEquiv

added def Matrix.reindexRingEquiv

added theorem Matrix.reindexRingEquiv_refl

added theorem Matrix.reindexRingEquiv_trans_reindexRingEquiv

added theorem Matrix.symm_reindexAddEquiv

added theorem Matrix.symm_reindexAlgEquiv

added theorem Matrix.symm_reindexLinearEquiv

added theorem Matrix.symm_reindexRingEquiv

added theorem Matrix.toAddEquiv_reindexAlgEquiv

added theorem Matrix.toAddEquiv_reindexLinearEquiv

added theorem Matrix.toAddEquiv_reindexRingEquiv

added theorem Matrix.toEquiv_reindexAddEquiv

added theorem Matrix.toEquiv_reindexAlgEquiv

added theorem Matrix.toEquiv_reindexLinearEquiv

added theorem Matrix.toEquiv_reindexRingEquiv

added theorem Matrix.toLinearEquiv_reindexAlgEquiv

added theorem Matrix.toRingEquiv_reindexAlgEquiv

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean