Theorem IsLocalization.map_algebraMap_ne_top_iff_disjoint

Modification history

2025-01-20 11:09
Mathlib/RingTheory/Localization/Ideal.lean
feat(RingTheory): prime is restriction of a prime iff it is the restriction of its extension (#20700) …
Added IsLocalization.map_algebraMap_ne_top_iff_disjointView on Github →