Theorems · Definition · algebraic topology
FundamentalGroup
(X : Type u_1) → [TopologicalSpace X] → X → Type u_1
The fundamental group is the automorphism group (vertex group) of the basepoint in the fundamental groupoid.
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 135 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
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.
- TopologicalSpacestatement and proof · cited by 24,529
- CategoryTheory.Endproof · cited by 169
Cited by49
Results whose statement or proof uses this declaration.
- IsCoveringMap.monodromyPermstatement and proof · cited by 11
- IsQuotientCoveringMap.fundamentalGroupToMulOppositestatement and proof · cited by 7
- IsAddQuotientCoveringMap.fundamentalGroupToMulOppositestatement · cited by 6
- FundamentalGroup.mapOfEqstatement · cited by 6
- IsQuotientCoveringMap.monodromy_eq_id_iffstatement and proof · cited by 3
- IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iffstatement and proof · cited by 2
- IsQuotientCoveringMap.ker_fundamentalGroupToMulOppositestatement and proof · cited by 2
- IsQuotientCoveringMap.ker_monodromyPermstatement and proof · cited by 2
- IsQuotientCoveringMap.monodromyPerm_injectivestatement and proof · cited by 2
- IsQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smulstatement and proof · cited by 2
- FundamentalGroup.fromPathstatement · cited by 2
- FundamentalGroup.mapstatement · cited by 2