Theorem TwoSidedIdeal.comap_le_comap

Modification history

2025-02-27 17:52
Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
feat(RingTheory/SimpleRing/Congr): simpleness is preserved by ring isomorphism (#21292) …
Added TwoSidedIdeal.comap_le_comapView on Github →