feat: port Data.Polynomial.Laurent (#2953)

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Moritz Firsching <firsching@google.com> Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>
leanprover-community · May 15, 2023 · c442325 · c442325
1 parent 31f0309
commit c442325
Show file tree

Hide file tree

Showing 2 changed files with 617 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1157,6 +1157,7 @@ import Mathlib.Data.Polynomial.Identities
 import Mathlib.Data.Polynomial.Induction
 import Mathlib.Data.Polynomial.Inductions
 import Mathlib.Data.Polynomial.IntegralNormalization
+import Mathlib.Data.Polynomial.Laurent
 import Mathlib.Data.Polynomial.Lifts
 import Mathlib.Data.Polynomial.Mirror
 import Mathlib.Data.Polynomial.Module