Commit 2023-05-18 07:49 bf2ce410

View on Github →

feat: port AlgebraicTopology.FundamentalGroupoid.FundamentalGroup (#4051)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

added def FundamentalGroup.fundamentalGroupMulEquivOfPath

added def FundamentalGroup.fundamentalGroupMulEquivOfPathConnected

added def FundamentalGroup