Theorem IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff

Modification history

2026-06-19 12:19
Mathlib/Topology/Homotopy/Lifting.lean
feat(Topology): `π₁(E⧸G) ≃* G` for `E` simply connected (#33108)
Added IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_IffView on Github →