Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-08 15:56 54ac48ad

View on Github →

chore(data/matrix/basic): add simp lemmas about minor, move reindex to matrix.basic since it knows nothing about linear algebra (#7083)

Estimated changes

Modified src/algebra/lie/classical.lean

Modified src/algebra/lie/matrix.lean

added theorem matrix.reindex_lie_equiv_symm

deleted theorem matrix.reindex_lie_equiv_symm_apply

Modified src/data/matrix/basic.lean

added theorem matrix.minor_add

added theorem matrix.minor_apply

added theorem matrix.minor_id_id

added theorem matrix.minor_minor

added theorem matrix.minor_neg

added theorem matrix.minor_smul

added theorem matrix.minor_sub

added theorem matrix.minor_zero

added def matrix.reindex

added theorem matrix.reindex_apply

added theorem matrix.reindex_refl_refl

added theorem matrix.reindex_symm

added theorem matrix.reindex_trans

added theorem matrix.transpose_minor

added theorem matrix.transpose_reindex

Modified src/linear_algebra/determinant.lean

added theorem matrix.det_minor_equiv_self

added theorem matrix.det_reindex_self

Modified src/linear_algebra/matrix.lean

deleted theorem matrix.coe_reindex_alg_equiv

deleted theorem matrix.coe_reindex_alg_equiv_symm

deleted theorem matrix.coe_reindex_linear_equiv

deleted theorem matrix.coe_reindex_linear_equiv_symm

deleted theorem matrix.det_reindex_self'

deleted theorem matrix.det_reindex_self

deleted def matrix.reindex

modified theorem matrix.reindex_alg_equiv_refl

added theorem matrix.reindex_alg_equiv_symm

deleted theorem matrix.reindex_alg_equiv_symm_apply

deleted theorem matrix.reindex_apply

modified theorem matrix.reindex_linear_equiv_apply

modified theorem matrix.reindex_linear_equiv_refl_refl

added theorem matrix.reindex_linear_equiv_symm

deleted theorem matrix.reindex_linear_equiv_symm_apply

deleted theorem matrix.reindex_refl_refl

deleted theorem matrix.reindex_symm_apply

deleted theorem matrix.reindex_transpose