Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-18 09:27 907147ad

View on Github →

feat(linear_algebra/matrix): define equivalences for reindexing matrices with equivalent types (#3409)

Estimated changes

Modified src/algebra/lie_algebra.lean

added def matrix.reindex_lie_equiv

added theorem matrix.reindex_lie_equiv_apply

added theorem matrix.reindex_lie_equiv_symm_apply

Modified src/linear_algebra/matrix.lean

added def matrix.reindex

added def matrix.reindex_alg_equiv

added theorem matrix.reindex_alg_equiv_apply

added theorem matrix.reindex_alg_equiv_symm_apply

added theorem matrix.reindex_apply

added def matrix.reindex_linear_equiv

added theorem matrix.reindex_linear_equiv_apply

added theorem matrix.reindex_linear_equiv_symm_apply

added theorem matrix.reindex_mul

added theorem matrix.reindex_symm_apply