mathlib3

c78ee2be - feat(data/polynomial/ring_division): add `roots_pow`, `roots_monomial` (#17663)

feat(data/polynomial/ring_division): add `roots_pow`, `roots_monomial` (#17663) * Add `polynomial.roots_pow`, `polynomial.roots_X_pow`, `polynomial.roots_C_mul_X_pow`, and `polynomial.roots_monomial`. * Golf some proofs.