Theorem Ideal.eq_bot_of_comap_eq_bot'

Modification history

2026-03-09 18:09
Mathlib/RingTheory/Ideal/Maps.lean
feat(Ringtheory/DedekindDomain): add RingEquiv lemmas (#35532) …
Added Ideal.eq_bot_of_comap_eq_bot'View on Github →