Mathlib Changelog
v4
Changelog
About
Github
Theorem
Localization.awayMap_bijective_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_bijective_of_dvd
View on Github →