Commit 2025-09-03 09:57 3b3f2146

View on Github →

feat(RingTheory/Polynomial): define discriminant (#29252)

Estimated changes

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

added theorem Polynomial.disc_C

added theorem Polynomial.disc_of_degree_eq_one

added theorem Polynomial.disc_of_degree_eq_two

added theorem Polynomial.resultant_deriv

added theorem Polynomial.sylvesterDeriv_updateRow