feat: port RingTheory.Int.Basic (#3014)

leanprover-community · Mar 21, 2023 · cff1de2 · cff1de2
1 parent 7c75134
commit cff1de2
Show file tree

Hide file tree

Showing 2 changed files with 421 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1288,6 +1288,7 @@ import Mathlib.RingTheory.Ideal.IdempotentFg
 import Mathlib.RingTheory.Ideal.Operations
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Int.Basic
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.Localization.Integer
 import Mathlib.RingTheory.Multiplicity