Commit 2026-06-19 12:19 6d8c7557

View on Github →

feat(Topology): π₁(E⧸G) ≃* G for E simply connected (#33108)

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

added theorem FundamentalGroup.inv_def

modified theorem FundamentalGroup.mapOfEq_apply

added theorem FundamentalGroup.mul_def

added theorem FundamentalGroup.one_def

deleted def FundamentalGroup

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

added theorem IsCoveringMap.coe_monodromyPerm

added def IsCoveringMap.fundamentalGroupMulAction

added theorem IsCoveringMap.homotopicRel_liftPath

added def IsCoveringMap.liftHomotopy

added def IsCoveringMap.liftHomotopyRel

added def IsCoveringMap.liftPath

added def IsCoveringMap.liftPathQuotient

added theorem IsCoveringMap.map_liftPathQuotient

added def IsCoveringMap.monodromy

added def IsCoveringMap.monodromyFunctor

added def IsCoveringMap.monodromyPerm

added theorem IsCoveringMap.monodromy_eq_of_map_eq

added theorem IsQuotientCoveringMap.commute_monodromyPerm_toPermFiber

added def IsQuotientCoveringMap.fundamentalGroupEquiv

added def IsQuotientCoveringMap.fundamentalGroupToMulOpposite

added theorem IsQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff

added theorem IsQuotientCoveringMap.fundamentalGroupToMulOpposite_eq_one_iff

added theorem IsQuotientCoveringMap.fundamentalGroupToMulOpposite_injective

added theorem IsQuotientCoveringMap.fundamentalGroupToMulOpposite_surjective

added theorem IsQuotientCoveringMap.ker_fundamentalGroupToMulOpposite

added theorem IsQuotientCoveringMap.ker_monodromyPerm

added theorem IsQuotientCoveringMap.monodromyPerm_injective

added theorem IsQuotientCoveringMap.monodromy_eq_id_iff

added theorem IsQuotientCoveringMap.monodromy_ext_iff

added theorem IsQuotientCoveringMap.monodromy_toPermFiber

added theorem IsQuotientCoveringMap.unop_fundamentalGroupToMulOpposite_smul