address comments

Author: wwylele

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -930,7 +930,7 @@ def subringCongr (h : s = t) : s ≃+* t :=
 
 @[simp]
 theorem subringCongr_symm (h : s = t) :
-    (subringCongr h).symm = subringCongr (h.symm) := rfl
+    (subringCongr h).symm = subringCongr h.symm := rfl
 
 @[simp]
 theorem coe_subringCongr_apply (h : s = t) (x : s) :

Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean

@@ -90,7 +90,7 @@ theorem Ideal.Quotient.isUnit_mk_pow_iff_notMem [I.IsMaximal] {n : ℕ} (hn : n
   rw [isUnit_mk_pow_iff_isUnit_mk I hn, isUnit_iff_ne_zero]
   exact Ideal.Quotient.eq_zero_iff_mem.not
 
-theorem Ideal.Quotient.notMem_of_isUnit_mk_pow [I.IsMaximal] {n : ℕ} {x : S} (hx : x ∉ I) :
+theorem Ideal.Quotient.isUnit_mk_pow_of_notMem [I.IsMaximal] {n : ℕ} {x : S} (hx : x ∉ I) :
     IsUnit (mk (I ^ n) x) := by
   by_cases! hn : n = 0
   · rw [pow_eq_top_iff.mpr (Or.inr hn)]

Mathlib/RingTheory/Localization/AtPrime/Basic.lean

@@ -526,15 +526,14 @@ theorem equivQuotMaximalIdeal_symm_apply_mk (x : R) (s : p.primeCompl) :
 @[deprecated (since := "2025-11-13")] alias _root_.equivQuotMaximalIdealOfIsLocalization :=
   equivQuotMaximalIdeal
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The isomorphism `R ⧸ p ^ n ≃+* Rₚ ⧸ maximalIdeal Rₚ ^ n`, where `Rₚ` satisfies
 `IsLocalization.AtPrime Rₚ p`. -/
 noncomputable
 def equivQuotMaximalIdealPow (n : ℕ) : R ⧸ p ^ n ≃+* Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ ^ n := by
   refine Subring.topEquiv.symm.trans <| -- R ⧸ p ^ n ≃ (⊤ : Subring (R ⧸ p ^ n))
     (RingEquiv.subringCongr ?_).trans <| -- ⊤ = (R ⧸ p ^ n ← Rₚ / ker).range
     (IsLocalization.lift fun (u : p.primeCompl) ↦ -- (R ⧸ p ^ n ← Rₚ) => R ⧸ p ^ n ← Rₚ / ker
-      Ideal.Quotient.notMem_of_isUnit_mk_pow _
+      Ideal.Quotient.isUnit_mk_pow_of_notMem _
       (mem_primeCompl_iff.mp u.prop)).quotientKerEquivRange.symm.trans <|
     quotEquivOfEq ?_ -- ker = maximalIdeal ^ n
   · symm
@@ -563,6 +562,23 @@ theorem equivQuotMaximalIdealPow_apply_mk (n : ℕ) (x : R) :
   ext
   simp
 
+/-- `IsLocalization.AtPrime.equivQuotMaximalIdealPow p Rₚ n` as an `R`-algebra isomorphism. -/
+noncomputable
+def equivQuotMaximalIdealPowₐ (n : ℕ) : (R ⧸ p ^ n) ≃ₐ[R] Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ ^ n
+    where
+  __ := equivQuotMaximalIdealPow p Rₚ n
+  commutes' r := by simp
+
+@[simp]
+theorem equivQuotMaximalIdealPowₐ_toRingEquiv (n : ℕ) :
+    (equivQuotMaximalIdealPowₐ p Rₚ n).toRingEquiv = equivQuotMaximalIdealPow p Rₚ n :=
+  rfl
+
+@[simp]
+theorem coe_equivQuotMaximalIdealPowₐ (n : ℕ) :
+    ⇑(equivQuotMaximalIdealPowₐ p Rₚ n) = ⇑(equivQuotMaximalIdealPow p Rₚ n) :=
+  rfl
+
 variable {Sₚ : Type*} [CommRing S] [Algebra R S] [CommRing Sₚ] [Algebra S Sₚ] [Algebra R Sₚ]
 variable [Algebra Rₚ Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
 variable [IsScalarTower R S Sₚ]