Theorem IsLocalization.algebraMap_mem_map_algebraMap_iff

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.algebraMap_mem_map_algebraMap_iffView on Github →