Def IsLocalization.AtPrime.orderIsoOfPrime

Modification history

2024-03-14 18:30
Mathlib/RingTheory/Localization/AtPrime.lean
feat(RingTheory/Localization): add facts about localization at minimal prime ideals (#11201) …
Added IsLocalization.AtPrime.orderIsoOfPrimeView on Github →