Theorem IsLocalization.Away.algebraMap_surjective_of_isIdempotentElem

Modification history

2026-02-10 18:25
Mathlib/RingTheory/Localization/Away/Basic.lean
feat(RingTheory): etale local structure of quasi-finite algebras (#35036)
Added IsLocalization.Away.algebraMap_surjective_of_isIdempotentElemView on Github →