feat: port RingTheory.MvPolynomial.WeightedHomogeneous (#3192)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Mar 31, 2023 · c04b29d · c04b29d
1 parent 3ba9781
commit c04b29d
Show file tree

Hide file tree

Showing 2 changed files with 466 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1392,6 +1392,7 @@ import Mathlib.RingTheory.Localization.NumDen
 import Mathlib.RingTheory.Multiplicity
 import Mathlib.RingTheory.MvPolynomial.Symmetric
 import Mathlib.RingTheory.MvPolynomial.Tower
+import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 import Mathlib.RingTheory.Nilpotent
 import Mathlib.RingTheory.Noetherian
 import Mathlib.RingTheory.NonZeroDivisors