Commit 2024-07-22 17:11 b9f14eb6

View on Github →

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

Estimated changes

Modified Mathlib/Algebra/Lie/Classical.lean

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

Modified Mathlib/LinearAlgebra/Matrix/Reindex.lean

modified theorem Matrix.det_reindexAlgEquiv

modified def Matrix.reindexAlgEquiv

modified theorem Matrix.reindexAlgEquiv_apply

modified theorem Matrix.reindexAlgEquiv_mul

modified theorem Matrix.reindexAlgEquiv_refl

modified theorem Matrix.reindexAlgEquiv_symm

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean