Def IsQuotientCoveringMap.fundamentalGroupToMulOpposite

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 View on Github →