Theorem Localization.awayMap_awayMap_surjective

Modification history

2026-02-10 18:25

Mathlib/RingTheory/Localization/Away/Basic.lean

feat(RingTheory): etale local structure of quasi-finite algebras (#35036)

Added Localization.awayMap_awayMap_surjective View on Github →