Theorem IsAddQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smul

Modification history

2026-06-23 16:50
Mathlib/Topology/Homotopy/Lifting.lean
feat: `π₁(E⧸G) ≃* Multiplicative G` for `E` simply connected (#40947) …
Added IsAddQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smulView on Github →