Def RingCon.comap

Modification history

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 →