Theorem Polynomial.Monic.roots_map_of_card_eq_natDegree

feat(Algebra/Polynomial/Roots): for a monic polynomial `p`, `p.roots.map f = (p.map f).roots` if `p.roots.card = p.natDegree` (#19430) …