Def RingCon.comap

Modification history

2025-11-26 15:01
Mathlib/RingTheory/Congruence/Defs.lean
feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences (#26277) …
Modified RingCon.comapView on Github →
2024-10-29 15:17
Mathlib/RingTheory/Congruence/Basic.lean
chore(RingTheory/Congruence): split off `Defs.lean` (#18387) …
Modified RingCon.comapView on Github →
2024-10-01 14:00
Mathlib/RingTheory/Congruence/Basic.lean
feat(RingTheory/TwoSidedIdeal): add some basic operations on two-sided-ideals (#14460)
Added RingCon.comapView on Github →