feat: port RingTheory.Polynomial.Content (#3066)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
leanprover-community · Mar 24, 2023 · 31b4870 · 31b4870
1 parent 90fa71a
commit 31b4870
Show file tree

Hide file tree

Showing 2 changed files with 522 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1350,6 +1350,7 @@ import Mathlib.RingTheory.NonZeroDivisors
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet
 import Mathlib.RingTheory.Polynomial.Chebyshev
+import Mathlib.RingTheory.Polynomial.Content
 import Mathlib.RingTheory.Polynomial.Opposites
 import Mathlib.RingTheory.Polynomial.Pochhammer
 import Mathlib.RingTheory.Polynomial.ScaleRoots