mathlib3

866664b8 - feat(data/polynomial/ring_division): add bUnion_roots_finite (#16670)

feat(data/polynomial/ring_division): add bUnion_roots_finite (#16670) Add three lemmas about polynomials needed for #15143 From flt-regular Co-authored-by: Damiano Testa <adomani@gmail.com>