Theorems · Definition · group theory
PresentedGroup.mk
{α : Type u_1} → (rels : Set (FreeGroup α)) → FreeGroup α →* PresentedGroup relsThe canonical map from the free group on α to a presented group with generators x : α,
where x is mapped to its equivalence class under the given set of relations rels
- Defined in
- Mathlib.GroupTheory.PresentedGroup
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- MonoidHomstatement · cited by 3,629
- QuotientGroup.mkproof · cited by 196
- FreeGroupstatement and proof · cited by 132
- PresentedGroupstatement · cited by 21
Cited by11
Results whose statement or proof uses this declaration.
- PresentedGroup.ofproof · cited by 12
- CoxeterSystem.simple_mul_simple_selfproof · cited by 9
- PresentedGroup.one_of_memstatement · cited by 3
- PresentedGroup.lift_toCoprod_inl_eq_inl_mkstatement and proof · cited by 1
- PresentedGroup.lift_toCoprod_inr_eq_inr_mkstatement and proof · cited by 1
- PresentedGroup.mk_eq_one_iffstatement · cited by 1
- CoxeterSystem.simple_mul_simple_powproof · cited by 1
- PresentedGroup.mk_eq_mk_of_inv_mul_memstatement · cited by 0
- PresentedGroup.mk_eq_mk_of_mul_inv_memstatement · cited by 0
- PresentedGroup.mk_surjectivestatement · cited by 0
- PresentedGroup.induction_onstatement and proof · cited by 0