Theorems · Definition · group theory
FreeGroup.of
{α : Type u} → α → FreeGroup αof is the canonical injection from the type to the free group over that type by sending each
element to the equivalence class of the letter that is the element.
- Defined in
- Mathlib.GroupTheory.FreeGroup.Basic
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
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.
- FreeGroupstatement · cited by 132
- FreeGroup.mkproof · cited by 34
Cited by49
Results whose statement or proof uses this declaration.
- FreeAbelianGroup.ofproof · cited by 40
- FreeGroup.liftproof · cited by 32
- PresentedGroup.ofproof · cited by 12
- FreeAbelianGroup.lift_apply_ofproof · cited by 12
- CoxeterSystem.simple_mul_simple_selfproof · cited by 9
- FreeGroup.lift_apply_ofstatement · cited by 7
- FreeGroup.ext_homstatement and proof · cited by 6
- FreeGroup.range_lift_eq_closureproof · cited by 5
- IsFreeGroup.ofproof · cited by 4
- FreeGroup.lift_uniquestatement and proof · cited by 3
- FreeGroup.of_injectivestatement and proof · cited by 3
- freeGroupEquivCoprodIproof · cited by 3