Commit 2026-09-15 08:33 4b28110a

feat(Localization/AtPrime/Basic): upgrade equivQuotMaximalIdeal to an AlgEquiv (#39287) The definition IsLocalization.AtPrime.equivQuotMaximalIdealPow was added in #36783. The case with n = 1 is still important and interesting. I have upgraded it to an AlgEquiv using equivQuotMaximalIdealPow. This did break a few small things, because we need to bridge back to a RingEquiv in some places. I took the liberty to add some missing apply lemmas to ease fixing these proofs. Disclaimer: I used Claude to suggest the first shot and refined it from there.