Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-28 02:35 d04e3fc1

View on Github →

feat(linear_algebra/char_poly): relates the characteristic polynomial to trace, determinant, and dimension (#3536) adds lemmas about the number of fixed points of a permutation adds lemmas connecting the trace, determinant, and dimension of a matrix to its characteristic polynomial

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.scalar.commute

Modified src/group_theory/perm/cycles.lean

added theorem equiv.perm.fixed_point_card_lt_of_ne_one

added theorem equiv.perm.one_lt_nonfixed_point_card_of_ne_one

Created src/linear_algebra/char_poly/coeff.lean

added theorem char_matrix_apply_nat_degree

added theorem char_matrix_apply_nat_degree_le

added theorem char_poly_coeff_eq_prod_coeff_of_le

added theorem char_poly_degree_eq_dim

added theorem char_poly_monic

added theorem char_poly_monic_of_nontrivial

added theorem char_poly_nat_degree_eq_dim

added theorem char_poly_sub_diagonal_degree_lt

added theorem det_eq_sign_char_poly_coeff

added theorem det_of_card_zero

added theorem eval_det

added theorem mat_poly_equiv_eval

added theorem trace_eq_neg_char_poly_coeff

Modified src/linear_algebra/determinant.lean

added theorem matrix.alg_hom.map_det

added theorem matrix.ring_hom.map_det