Def Matrix.reindexAlgEquiv

Modification history

2026-03-26 22:21

Mathlib/LinearAlgebra/Matrix/Reindex.lean

chore(LinearAlgebra/Matrix): generalize equivs and use `where` (#37178) …

Modified Matrix.reindexAlgEquiv View on Github →

2024-07-22 17:11

Mathlib/LinearAlgebra/Matrix/Reindex.lean

chore(LinearAlgebra/Matrix/Reindex): generalize `reindexAlgEquiv` (#14823)

Modified Matrix.reindexAlgEquiv View on Github →

2023-04-20 15:22

Mathlib/LinearAlgebra/Matrix/Reindex.lean

feat: port LinearAlgebra.Matrix.Reindex (#3549)

Added Matrix.reindexAlgEquiv View on Github →