Commit 2023-04-20 15:22 604a91b3

View on Github →

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

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Reindex.lean

added theorem Matrix.det_reindexAlgEquiv

added theorem Matrix.det_reindexLinearEquiv_self

added theorem Matrix.mul_reindexLinearEquiv_one

added def Matrix.reindexAlgEquiv

added theorem Matrix.reindexAlgEquiv_apply

added theorem Matrix.reindexAlgEquiv_mul

added theorem Matrix.reindexAlgEquiv_refl

added theorem Matrix.reindexAlgEquiv_symm

added def Matrix.reindexLinearEquiv

added theorem Matrix.reindexLinearEquiv_apply

added theorem Matrix.reindexLinearEquiv_comp

added theorem Matrix.reindexLinearEquiv_comp_apply

added theorem Matrix.reindexLinearEquiv_mul

added theorem Matrix.reindexLinearEquiv_one

added theorem Matrix.reindexLinearEquiv_refl_refl

added theorem Matrix.reindexLinearEquiv_symm

added theorem Matrix.reindexLinearEquiv_trans