Commit 2025-10-08 20:10 b6e83e57

View on Github →

chore: rename polynomial lemmas (#30270) Renaming the lemmas Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits and Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split to agree with the equality order.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits

added theorem Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits

deleted theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits

deleted theorem Polynomial.sum_roots_eq_nextCoeff_of_monic_of_split

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

Modified Mathlib/RingTheory/Norm/Basic.lean

Modified Mathlib/RingTheory/Trace/Basic.lean