feat: port RingTheory.PrincipalIdealDomain (#3012)

leanprover-community · Mar 21, 2023 · 9d04f3c · 9d04f3c
1 parent d4cca00
commit 9d04f3c
Show file tree

Hide file tree

Showing 2 changed files with 570 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1301,6 +1301,7 @@ import Mathlib.RingTheory.Polynomial.Pochhammer
 import Mathlib.RingTheory.Polynomial.ScaleRoots
 import Mathlib.RingTheory.Polynomial.Tower
 import Mathlib.RingTheory.Prime
+import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.RingInvo
 import Mathlib.RingTheory.Subring.Basic
 import Mathlib.RingTheory.Subring.Pointwise