Theorem Localization.exists_awayMap_bijective_of_localRingHom_bijective

Modification history

2026-02-09 11:07
Mathlib/RingTheory/Unramified/LocalRing.lean
feat(RingTheory): local structure for finite unramified algebras (#34928)
Added Localization.exists_awayMap_bijective_of_localRingHom_bijectiveView on Github →