Commit 2025-07-02 03:33 fcc863c1

View on Github →

feat(RingTheory): resultant of two polynomials (#26285)

Estimated changes

Modified Mathlib.lean

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

added def Polynomial.resultant

added theorem Polynomial.resultant_C_right

added theorem Polynomial.resultant_C_zero_right

added def Polynomial.sylvester

added theorem Polynomial.sylvester_C_right