chore: split MvPolynomial.Variables (#11094)

Splits this file into two. The sections about `degree` related concepts are totally independent of the `vars` related concepts so this was a clean split.
leanprover-community · Mar 4, 2024 · 7f32cc7 · 7f32cc7
1 parent 8a0b321
commit 7f32cc7
Show file tree

Hide file tree

Showing 5 changed files with 587 additions and 528 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1832,6 +1832,7 @@ import Mathlib.Data.MvPolynomial.Cardinal
 import Mathlib.Data.MvPolynomial.Comap
 import Mathlib.Data.MvPolynomial.CommRing
 import Mathlib.Data.MvPolynomial.Counit
+import Mathlib.Data.MvPolynomial.Degrees
 import Mathlib.Data.MvPolynomial.Derivation
 import Mathlib.Data.MvPolynomial.Division
 import Mathlib.Data.MvPolynomial.Equiv