Theorem IsLocalization.Away.algebraMap_pow_isUnit

Modification history

2024-09-29 14:29
Mathlib/RingTheory/Localization/Away/Basic.lean
feat(RingTheory/Localization): some API on localizations (#17030) …
Added IsLocalization.Away.algebraMap_pow_isUnitView on Github →