Theorem FundamentalGroup.mapOfEq_apply

Modification history

2026-06-19 12:19
Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean
feat(Topology): `π₁(E⧸G) ≃* G` for `E` simply connected (#33108)
Modified FundamentalGroup.mapOfEq_applyView on Github →
2025-10-18 17:29
Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean
chore(AlgebraicTopology): clean up FundamentalGroupoid (#28234) …
Added FundamentalGroup.mapOfEq_applyView on Github →