Commit 2023-12-17 23:08 91ef6889

View on Github →

feat(Data/Polynomial/RingDivision): Negation lemmas for roots, aroots, and rootSet (#9133) This PR adds negation lemmas for roots, aroots, and rootSet.

Estimated changes

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.aroots_neg

added theorem Polynomial.rootSet_neg

added theorem Polynomial.rootSet_one

added theorem Polynomial.roots_neg