Theorem Ideal.map_comap_bot

Modification history

2026-09-26 10:13
Mathlib/RingTheory/Ideal/Maps.lean
feat(RingTheory/Ideal): the `⊥` and `⊤` cases of the pointwise action on ideals (#44070) …
Added Ideal.map_comap_botView on Github →