Theorem Matrix.GeneralLinearGroup.reindexMulEquiv_trans_reindexMulEquiv

Modification history

2026-11-10 21:51
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
chore(LinearAlgebra/Matrix): add api for compatibility between `reindex` and `map` for `GL` and `Matrix` (#45519)
Deleted Matrix.GeneralLinearGroup.reindexMulEquiv_trans_reindexMulEquivView on Github →
2026-10-28 01:55
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean
feat(LinearAlgebra/Matrix/GeneralLinearGroup/Defs): add `MulEquiv` for `GL` (#43945) …
Added Matrix.GeneralLinearGroup.reindexMulEquiv_trans_reindexMulEquivView on Github →