Theorem FundamentalGroup.one_def

Modification history

2026-10-04 10:20

Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

chore(CategoryTheory): `End` and `Aut` as `1`-field structures (#43759) …

Modified FundamentalGroup.one_def View on Github →

2026-06-19 12:19

Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

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

Added FundamentalGroup.one_def View on Github →