Theorem Matrix.reindexAlgEquiv_refl

Modification history

2024-07-22 17:11

Mathlib/LinearAlgebra/Matrix/Reindex.lean

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

Modified Matrix.reindexAlgEquiv_refl View on Github →

2023-04-20 15:22

Mathlib/LinearAlgebra/Matrix/Reindex.lean

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

Added Matrix.reindexAlgEquiv_refl View on Github →