Theorem IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_symm_apply_mk

Modification history

2026-09-15 08:33
Mathlib/RingTheory/Localization/AtPrime/Basic.lean
feat(Localization/AtPrime/Basic): upgrade `equivQuotMaximalIdeal` to an AlgEquiv (#39287) …
Added IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_symm_apply_mkView on Github →