Commit 2026-10-23 13:54 1a88f03d
View on Github →refactor(Algebra/Polynomial): improve characterisation of p.roots = 0 (#44237)
- Change statements of
Polynomial.roots_eq_zero_iff_*to be more usable - Add versions for
p.roots ≠ 0(+ an analogue for bare multisets) - Make use of these characterisations downstream (+ incidental golfs)
The old lemmas have been deprecated without direct replacement. This is because the new lemmas are more usable and because the old lemmas were not used anywhere in Mathlib. The old lemmas had
p.IsRoot = ⊥on the RHS, which uses the lattice instance on Pi types and is difficult to rewrite with.