Def Matrix.reindexLinearEquiv

Modification history

2026-03-26 22:21

Mathlib/LinearAlgebra/Matrix/Reindex.lean

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

Modified Matrix.reindexLinearEquiv View on Github →

2023-04-20 15:22

Mathlib/LinearAlgebra/Matrix/Reindex.lean

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

Added Matrix.reindexLinearEquiv View on Github →