Def FundamentalGroup

Modification history

2026-06-19 12:19

Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

feat(Topology): `π₁(E⧸G) ≃* G` for `E` simply connected (#33108)

Deleted FundamentalGroup View on Github →

2025-10-18 17:29

Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

chore(AlgebraicTopology): clean up FundamentalGroupoid (#28234) …

Modified FundamentalGroup View on Github →

2023-05-18 07:49

Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

feat: port AlgebraicTopology.FundamentalGroupoid.FundamentalGroup (#4051)

Added FundamentalGroup View on Github →