Commit 2023-11-08 18:36 6b362d1e

View on Github →

fix: Fix FundamentalGroupoid being reducible. (#8257) Instead it is now the opposite -- a structure with a single field. zulip discussion

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

added def FundamentalGroupoid.equiv

modified def FundamentalGroupoid.fromPath

modified def FundamentalGroupoid.fromTop

modified theorem FundamentalGroupoid.id_eq_path_refl

added theorem FundamentalGroupoid.isEmpty_iff

added theorem FundamentalGroupoid.nonempty_iff

added theorem FundamentalGroupoid.subsingleton_iff

modified def FundamentalGroupoid.toPath

modified def FundamentalGroupoid.toTop

added structure FundamentalGroupoid

deleted def FundamentalGroupoid

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

modified theorem ContinuousMap.Homotopy.hcast_def

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean