Theorems · Definition · group theory
Con.toQuotient
{M : Type u_1} → [inst : Mul M] → {c : Con M} → M → c.QuotientThe morphism into the quotient by a congruence relation
- Defined in
- Mathlib.GroupTheory.Congruence.Defs
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Constatement and proof · cited by 152
- Quotient.mk''proof · cited by 132
- Con.Quotientstatement · cited by 48
Cited by38
Results whose statement or proof uses this declaration.
- Con.eqstatement · cited by 9
- Con.hom_extproof · cited by 3
- Con.lift_rangeproof · cited by 2
- Con.mkMulHomproof · cited by 2
- Con.quotientKerEquivOfRightInverseproof · cited by 2
- Con.hrecOn₂statement and proof · cited by 1
- Con.induction_onstatement and proof · cited by 1
- Con.liftOnUnitsproof · cited by 1
- Con.lift_apply_mk'statement and proof · cited by 1
- Con.map_of_mul_left_rel_oneproof · cited by 1
- Con.coe_dfinsuppProdstatement · cited by 1
- Con.coe_finsetProdstatement · cited by 1