Commit 2024-10-01 19:58 3a0cb01a

View on Github →

chore: rename Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split (#17337)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Splits.lean

deleted theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_split

added theorem Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits

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

Modified Mathlib/RingTheory/Norm/Basic.lean