Commit 2026-06-23 16:50 778bd8fa

View on Github →

feat: π₁(E⧸G) ≃* Multiplicative G for E simply connected (#40947) This is the additive version of #33108

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added theorem Additive.mulAction_orbit

added theorem Multiplicative.mulAction_orbit

Modified Mathlib/Topology/Covering/Quotient.lean

added theorem IsAddQuotientCoveringMap.toMultiplicative

added theorem IsQuotientCoveringMap.toAdditive

Modified Mathlib/Topology/Homotopy/Lifting.lean

added theorem IsAddQuotientCoveringMap.commute_monodromyPerm_toPermFiber

added def IsAddQuotientCoveringMap.fundamentalGroupEquiv

added def IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite

added theorem IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff

added theorem IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_eq_one_iff

added theorem IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_injective

added theorem IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_surjective

added theorem IsAddQuotientCoveringMap.ker_fundamentalGroupToMulOpposite

added theorem IsAddQuotientCoveringMap.ker_monodromyPerm

added theorem IsAddQuotientCoveringMap.monodromyPerm_injective

added theorem IsAddQuotientCoveringMap.monodromy_eq_id_iff

added theorem IsAddQuotientCoveringMap.monodromy_ext_iff

added theorem IsAddQuotientCoveringMap.monodromy_toPermFiber

added theorem IsAddQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smul