Commit 2024-11-30 00:03 6ce78a15
View on Github →feat(Algebra/Polynomial/Roots): for a monic polynomial p
, p.roots.map f = (p.map f).roots
if p.roots.card = p.natDegree
(#19430)
A variant of the theorem Polynomial.roots_map_of_injective_of_card_eq_natDegree that replaces the injectivity condition with p.Monic
.