Theorems · Theorem · group theory
Con.comap_eq
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {c : Con M} {f : N →* M},
Con.comap ⇑f ⋯ c = Con.ker (c.mk'.comp f)Given a monoid homomorphism f : N → M and a congruence relation c on M, the congruence
relation induced on N by f equals the kernel of c's quotient homomorphism composed with
f.
- Defined in
- Mathlib.GroupTheory.Congruence.Hom
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
- Assumes
- MulOneClassMulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- MonoidHomstatement and proof · cited by 3,629
- MulOneClassstatement and proof · cited by 1,018
- MonoidHom.compstatement · cited by 469
- Constatement and proof · cited by 152
- Con.Quotientstatement · cited by 48
- MonoidHom.map_mulstatement · cited by 37
- Con.kerstatement · cited by 24
- Con.mk'statement and proof · cited by 22
- Con.comapstatement · cited by 15
- Con.eqproof · cited by 9
- Con.extproof · cited by 8
Cited by2
Results whose statement or proof uses this declaration.
- Con.comapQuotientEquivOfSurjproof · cited by 3
- Con.comapQuotientEquivproof · cited by 0