Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-26 10:39 453f2183

View on Github →

refactor(linear_algebra/charpoly): move linear_algebra/charpoly to linear_algebra/matrix/charpoly (#9368) We move linear_algebra/charpolyto linear_algebra/matrix/charpoly, since the results there are for matrices. We also rename some lemmas in linear_algebra/matrix/charpoly/coeff to have the namespace matrix.

Estimated changes

Modified archive/100-theorems-list/83_friendship_graphs.lean

Modified docs/100.yaml

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified src/linear_algebra/charpoly.lean

Renamed src/linear_algebra/charpoly/basic.lean to src/linear_algebra/matrix/charpoly/basic.lean

deleted theorem aeval_self_charpoly

added theorem matrix.aeval_self_charpoly

Renamed src/linear_algebra/charpoly/coeff.lean to src/linear_algebra/matrix/charpoly/coeff.lean

deleted theorem charpoly_coeff_eq_prod_coeff_of_le

deleted theorem charpoly_degree_eq_dim

deleted theorem charpoly_monic

deleted theorem charpoly_nat_degree_eq_dim

deleted theorem charpoly_sub_diagonal_degree_lt

deleted theorem det_eq_sign_charpoly_coeff

deleted theorem det_of_card_zero

deleted theorem eval_det

deleted theorem finite_field.charpoly_pow_card

added theorem finite_field.matrix.charpoly_pow_card

deleted theorem mat_poly_equiv_eval

added theorem matrix.charpoly_coeff_eq_prod_coeff_of_le

added theorem matrix.charpoly_degree_eq_dim

added theorem matrix.charpoly_monic

added theorem matrix.charpoly_nat_degree_eq_dim

added theorem matrix.charpoly_sub_diagonal_degree_lt

added theorem matrix.det_eq_sign_charpoly_coeff

added theorem matrix.det_of_card_zero

added theorem matrix.eval_det

added theorem matrix.mat_poly_equiv_eval

added theorem matrix.trace_eq_neg_charpoly_coeff

deleted theorem trace_eq_neg_charpoly_coeff

Modified src/ring_theory/norm.lean

Modified src/ring_theory/trace.lean