Theorem Matrix.GeneralLinearGroup.reindexMulEquiv_refl

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_refl View 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_refl View on Github →