mathlib3

255862e2 - refactor(linear_algebra/char_poly/basic): rename char_poly to matrix.charpoly (#9230)

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`).