Theorems · Definition · group theory
Con.Quotient
{M : Type u_1} → [inst : Mul M] → Con M → Type u_1Defining the quotient by a congruence relation of a type with a multiplication.
- Defined in
- Mathlib.GroupTheory.Congruence.Defs
- Cited by
- 48 results in Mathlib
- Foundations
- Depth 3 from the axioms · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Constatement and proof · cited by 152
- Con.toSetoidproof · cited by 38
Cited by72
Results whose statement or proof uses this declaration.
- Monoid.Coprodproof · cited by 109
- Monoid.CoprodIproof · cited by 52
- Con.toQuotientstatement · cited by 33
- Monoid.PushoutIproof · cited by 30
- HNNExtensionproof · cited by 26
- Con.mk'statement and proof · cited by 22
- Localization.monoidOfproof · cited by 17
- Con.liftstatement and proof · cited by 12
- PresentedMonoidproof · cited by 10
- Con.eqstatement · cited by 9
- Con.kerLiftstatement · cited by 4
- Con.mk'_surjectivestatement · cited by 4