chore(data/polynomial/degree): consolidate all polynomial.degree fi…

…les in one folder (#5005) Moves `data/polynomial/degree.lean` to `data/polynomial/degree`, which already exists, renames it `lemmas.lean` Renames `data/polynomial/degree/basic.lean` to `definitions.lean` Adds `data/polynomial/degree/default.lean`, which just imports `lemmas.lean`
leanprover-community · Nov 15, 2020 · 447b18f · 447b18f
1 parent fca7eba
commit 447b18f
Show file tree

Hide file tree

Showing 8 changed files with 4 additions and 5 deletions.
diff --git a/src/data/polynomial/cancel_leads.lean b/src/data/polynomial/cancel_leads.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import data.polynomial.degree.basic
+import data.polynomial.degree.definitions
 
 /-!
 # Cancel the leading terms of two polynomials

diff --git a/src/data/polynomial/degree/default.lean b/src/data/polynomial/degree/default.lean
@@ -0,0 +1 @@
+import data.polynomial.degree.lemmas
diff --git a/src/data/polynomial/degree/basic.lean → src/data/polynomial/degree/definitions.lean b/src/data/polynomial/degree/basic.lean → src/data/polynomial/degree/definitions.lean
diff --git a/src/data/polynomial/degree.lean → src/data/polynomial/degree/lemmas.lean b/src/data/polynomial/degree.lean → src/data/polynomial/degree/lemmas.lean
diff --git a/src/data/polynomial/degree/trailing_degree.lean b/src/data/polynomial/degree/trailing_degree.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.polynomial.degree.basic
+import data.polynomial.degree.definitions
 
 /-!
 # Trailing degree of univariate polynomials

diff --git a/src/data/polynomial/erase_lead.lean b/src/data/polynomial/erase_lead.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import data.polynomial.degree.basic
 import data.polynomial.degree
 import data.polynomial.degree.trailing_degree
 

diff --git a/src/data/polynomial/eval.lean b/src/data/polynomial/eval.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 -/
 import data.polynomial.induction
-import data.polynomial.degree.basic
+import data.polynomial.degree.definitions
 import deprecated.ring
 
 /-!

diff --git a/src/data/polynomial/lifts.lean b/src/data/polynomial/lifts.lean
@@ -8,7 +8,6 @@ import data.polynomial.algebra_map
 import algebra.algebra.subalgebra
 import algebra.polynomial.big_operators
 import data.polynomial.erase_lead
-import data.polynomial.degree.basic
 
 /-!
 # Polynomials that lift