Theorem RingHom.map_ker

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