Commit 2025-11-25 07:45 09d878bb

View on Github →

feat(RingTheory): resultant is in the span of the two polynomials (#31864)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem WithBot.bot_lt_natCast

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

added def Polynomial.adjSylvester

added theorem Polynomial.adjSylvester_comp_sylveserMap

added theorem Polynomial.exists_mul_add_mul_eq_C_resultant

added theorem Polynomial.sylveserMap_comp_adjSylvester

added def Polynomial.sylvesterMap

added theorem Polynomial.toMatrix_sylvesterMap'

added theorem Polynomial.toMatrix_sylvesterMap