Commit 2021-06-22 10:22 9ca85977

View on Github →

feat(linear_algebra/matrix/reindex): add some lemmas (#7963) From LTE Added lemmas reindex_linear_equiv_trans, reindex_linear_equiv_comp, reindex_linear_equiv_comp_apply, reindex_linear_equiv_one and mul_reindex_linear_equiv_mul_one needed in LTE.

Estimated changes

Modified src/data/matrix/basic.lean

modified def matrix.minor

modified theorem matrix.minor_apply

added theorem matrix.mul_minor_one

added theorem matrix.one_minor_mul

modified theorem matrix.transpose_minor

Modified src/linear_algebra/matrix/reindex.lean

added theorem matrix.mul_reindex_linear_equiv_one

added theorem matrix.reindex_linear_equiv_comp

added theorem matrix.reindex_linear_equiv_comp_apply

modified theorem matrix.reindex_linear_equiv_mul

added theorem matrix.reindex_linear_equiv_one

added theorem matrix.reindex_linear_equiv_trans