Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-18 11:42 55e2dfde

View on Github →

chore(data.matrix): rename minor to submatrix (#16101) As discussed on Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/matrix.2Eminor.20wrong.20terminology.3F This is an alternative to the previous plan to rename minor to on in #16063. Moreover, I have adapted some documentation in src/linear_algebra/matrix/adjugate.lean that also used the term "minor" in the wrong way.

Estimated changes

deleted theorem matrix.diag_minor
added theorem matrix.diag_submatrix
deleted def matrix.minor
deleted theorem matrix.minor_add
deleted theorem matrix.minor_apply
deleted theorem matrix.minor_diagonal
deleted theorem matrix.minor_id_id
deleted theorem matrix.minor_map
deleted theorem matrix.minor_minor
deleted theorem matrix.minor_mul
deleted theorem matrix.minor_mul_equiv
deleted theorem matrix.minor_neg
deleted theorem matrix.minor_one
deleted theorem matrix.minor_one_equiv
deleted theorem matrix.minor_smul
deleted theorem matrix.minor_sub
deleted theorem matrix.minor_zero
deleted theorem matrix.mul_minor_one
deleted theorem matrix.one_minor_mul
added def matrix.submatrix
added theorem matrix.submatrix_add
added theorem matrix.submatrix_apply
added theorem matrix.submatrix_id_id
added theorem matrix.submatrix_map
added theorem matrix.submatrix_mul
added theorem matrix.submatrix_neg
added theorem matrix.submatrix_one
added theorem matrix.submatrix_smul
added theorem matrix.submatrix_sub
added theorem matrix.submatrix_zero
deleted theorem matrix.transpose_minor
deleted theorem matrix.minor_cons_row
deleted theorem matrix.minor_empty
added theorem matrix.submatrix_empty
deleted theorem matrix.is_hermitian.minor
deleted theorem matrix.is_diag.minor
deleted theorem matrix.is_symm.minor
deleted theorem continuous.matrix_minor