Mathlib v3 is deprecated. Go to Mathlib v4

Theorem coeff_charpoly_mem_ideal_pow

Modification history

2022-07-17 19:11

src/linear_algebra/matrix/charpoly/coeff.lean

feat(linear_algebra/matrix/charpoly): Coefficients of the characteristic polynomial falls in the ideal power. (#15459)

Added coeff_charpoly_mem_ideal_pow View on Github →