mathlib

ea961f76 - chore(ring_theory/polynomial): move `ring_theory.polynomial` to `ring_theory.polynomial.basic` (#3248)

chore(ring_theory/polynomial): move `ring_theory.polynomial` to `ring_theory.polynomial.basic` (#3248) This PR is the intersection of #3223 and #3241, allowing them to be merged in either order. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/where.20should.20these.20definitions.20live.3F Co-authored-by: Johan Commelin <johan@commelin.net>