feat: port Data.MvPolynomial.Basic (#2861)

leanprover-community · Mar 15, 2023 · ac78b1d · ac78b1d
1 parent 8be9b2d
commit ac78b1d
Show file tree

Hide file tree

Showing 2 changed files with 1,608 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -713,6 +713,7 @@ import Mathlib.Data.Multiset.Range
 import Mathlib.Data.Multiset.Sections
 import Mathlib.Data.Multiset.Sort
 import Mathlib.Data.Multiset.Sum
+import Mathlib.Data.MvPolynomial.Basic
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.Nat.Bitwise