Theorems · Definition · group theory
QuotientGroup.mk
{α : Type u_1} → [inst : Group α] → {s : Subgroup α} → α → α ⧸ sThe canonical map from a group α to the quotient α ⧸ s.
- Defined in
- Mathlib.GroupTheory.Coset.Defs
- Cited by
- 196 results in Mathlib
- Foundations
- Depth 68 from the axioms, rests on 827 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Subgroupstatement and proof · cited by 3,593
- HasQuotient.Quotientstatement · cited by 2,301
- Quotient.mk''proof · cited by 132
Cited by215
Results whose statement or proof uses this declaration.
- QuotientGroup.mk'proof · cited by 90
- Abelianization.ofproof · cited by 20
- QuotientGroup.eqstatement · cited by 20
- QuotientGroup.eq_one_iffstatement · cited by 18
- Subgroup.IsComplement.leftQuotientEquivproof · cited by 17
- QuotientGroup.induction_onstatement and proof · cited by 17
- QuotientGroup.mk_surjectivestatement · cited by 12
- PresentedGroup.mkproof · cited by 10
- Subgroup.index_comap_of_surjectiveproof · cited by 5
- QuotientGroup.out_eq'statement · cited by 5
- QuotientGroup.out_conj_pow_minimalPeriod_memproof · cited by 4
- QuotientGroup.coe_mk'statement · cited by 4
Showing the 200 most cited of 215.