mathlib

6d7e7563 - feat(linear_algebra/char_poly): charpoly of `left_mul_matrix` (#7397)

feat(linear_algebra/char_poly): charpoly of `left_mul_matrix` (#7397) This is an important ingredient for showing the field norm resp. trace of `x` is the product resp. sum of `x`'s conjugates.