Theorem Polynomial.roots_map_of_map_ne_zero_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) …