Commit 2026-11-10 21:51 1db74aa2

View on Github →

chore(LinearAlgebra/Matrix): add api for compatibility between reindex and map for GL and Matrix (#45519)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Defs.lean

added theorem Matrix.reindex_map

Modified Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean

deleted theorem Matrix.GeneralLinearGroup.reindexMulEquiv_refl

deleted theorem Matrix.GeneralLinearGroup.reindexMulEquiv_trans_reindexMulEquiv

added theorem Matrix.GeneralLinearGroup.reindex_comp_map

added theorem Matrix.GeneralLinearGroup.reindex_map

added theorem Matrix.GeneralLinearGroup.reindex_refl

added theorem Matrix.GeneralLinearGroup.reindex_trans_mapEquiv

added theorem Matrix.GeneralLinearGroup.reindex_trans_reindex

added theorem Matrix.GeneralLinearGroup.symm_reindex

deleted theorem Matrix.GeneralLinearGroup.symm_reindexMulEquiv