fixing error after adding change

leanprover-community · Oct 30, 2024 · c6c8da1 · c6c8da1
1 parent 037ace6
commit c6c8da1
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean b/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean
@@ -128,7 +128,7 @@ noncomputable def nilradmaxlocalizationIsSelf [h : (nilradical R).IsMaximal] (h'
     [IsLocalization M S] : R ≃ₐ[R] S := by
   have (m) (hm : m ∈ M) : IsUnit m := by
     haveI := LocalRing.of_nilradical_isMaximal (h := h)
-    apply (LocalRing.not_mem_maximalIdeal m).mp
+    apply LocalRing.not_mem_maximalIdeal.mp
     rw [← LocalRing.eq_maximalIdeal h]
     rintro ⟨k, hk⟩
     rw [← hk] at h'