Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-02 04:27 6d7e7563

View on Github →

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.

Estimated changes