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>
leanprover-community · Jun 30, 2020 · ea961f7 · ea961f7
1 parent 9524dee
commit ea961f7
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 0 deletions.
diff --git a/src/ring_theory/polynomial.lean → src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial.lean → src/ring_theory/polynomial/basic.lean
diff --git a/src/ring_theory/polynomial/default.lean b/src/ring_theory/polynomial/default.lean
@@ -0,0 +1 @@
+import ring_theory.polynomial.basic