Theorem Ideal.comap_map_eq_self_iff_of_isPrime

Modification history

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