feat port RingTheory.JacobsonIdeal (#4061)

leanprover-community · May 18, 2023 · a3ae6e9 · a3ae6e9
1 parent 5a1d44a
commit a3ae6e9
Show file tree

Hide file tree

Showing 2 changed files with 414 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1815,6 +1815,7 @@ import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Ideal.QuotientOperations
 import Mathlib.RingTheory.Int.Basic
+import Mathlib.RingTheory.JacobsonIdeal
 import Mathlib.RingTheory.Localization.Basic
 import Mathlib.RingTheory.Localization.FractionRing
 import Mathlib.RingTheory.Localization.Ideal