Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 19:04 255862e2

View on Github →

refactor(linear_algebra/char_poly/basic): rename char_poly to matrix.charpoly (#9230) We rename char_matrix to charmatrix and char_poly to matrix.charpoly, so M.charpoly becomes available (and everything is coherent with minpoly).

Estimated changes

deleted theorem aeval_self_char_poly
added theorem aeval_self_charpoly
deleted def char_matrix
deleted theorem char_matrix_apply_eq
deleted theorem char_matrix_apply_ne
deleted def char_poly
added def charmatrix
added theorem charmatrix_apply_eq
added theorem charmatrix_apply_ne
added def matrix.charpoly
deleted theorem char_poly_degree_eq_dim
deleted theorem char_poly_left_mul_matrix
deleted theorem char_poly_monic
added theorem charpoly_degree_eq_dim
added theorem charpoly_monic
modified theorem matrix.is_integral
deleted theorem zmod.char_poly_pow_card
added theorem zmod.charpoly_pow_card