mathlib3

0fb4144a - feat(data/polynomial/ring_division,ring_theory/algebraic): Basic consequences of `x ∈ p.root_set` (#15745)

feat(data/polynomial/ring_division,ring_theory/algebraic): Basic consequences of `x ∈ p.root_set` (#15745) This PR adds two basic consequences of `x ∈ p.root_set`: `p ≠ 0` and `is_algebraic x`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>