Theorem Localization.awayMap_injective_of_dvd

Modification history

2026-02-10 16:30
Mathlib/RingTheory/Localization/Away/Basic.lean
feat(RingTheory): local structure of unramified algebras (#35023)
Added Localization.awayMap_injective_of_dvdView on Github →