Theorem Ideal.disjoint_map_primeCompl_iff_comap_le

Modification history

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