Commit 2024-11-30 00:03 6ce78a15

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.