Commit 2026-02-18 07:28 26636533

View on Github →

feat(Algebra/Polynomial/Lifts): Add mem_lifts_and_support_eq (#35132) mem_lifts_and_degree_eq was already proving the more general statement, so I extracted the proof. I need this for #34877.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Lifts.lean

added theorem Polynomial.exists_degree_eq_of_mem_lifts

added theorem Polynomial.exists_support_eq_of_mem_lifts

deleted theorem Polynomial.mem_lifts_and_degree_eq

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