From c6c8da1b168c4429599a08f2738e1b52462db921 Mon Sep 17 00:00:00 2001 From: maddycrim Date: Wed, 30 Oct 2024 12:27:41 -0400 Subject: [PATCH] fixing error after adding change --- Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean b/Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean index a878dc61dd274..52af57cabe602 100644 --- 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'