chore(RingTheory/Jacobson): Rename Ideal.IsJacobson to `IsJacobsonR…

…ing`. (#18271)
leanprover-community · Oct 31, 2024 · 2e82aa2 · 2e82aa2
1 parent c169023
commit 2e82aa2
Show file tree

Hide file tree

Showing 3 changed files with 212 additions and 144 deletions.
diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean
@@ -22,11 +22,11 @@ import Mathlib.RingTheory.Jacobson
 
 open Ideal
 
-variable {R : Type*} [CommRing R] [IsJacobson R]
+variable {R : Type*} [CommRing R] [IsJacobsonRing R]
 
 namespace PrimeSpectrum
 
-lemma exists_isClosed_singleton_of_isJacobson
+lemma exists_isClosed_singleton_of_isJacobsonRing
     (s : (Set (PrimeSpectrum R))) (hs : IsOpen s) (hs' : s.Nonempty) :
     ∃ x ∈ s, IsClosed {x} := by
   simp_rw [isClosed_singleton_iff_isMaximal]
@@ -48,12 +48,12 @@ If `R` is both noetherian and jacobson, then the following are equivalent for `x
 3. `{x}` is both closed and stable under generalization
   (i.e. `x` is both a minimal prime and a maximal ideal)
 -/
-lemma isOpen_singleton_tfae_of_isNoetherian_of_isJacobson
+lemma isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing
     [IsNoetherianRing R] (x : PrimeSpectrum R) :
     List.TFAE [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}] := by
   tfae_have 1 → 2
   · intro h
-    obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobson _ h
+    obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h
       ⟨x, Set.mem_singleton x⟩
     exact ⟨h', h⟩
   tfae_have 2 → 3