mathlib3

3a0532a8 - feat(topology/homotopy/fundamental_group): prove fundamental group is independent of basepoint in path-connected spaces (#12234)

feat(topology/homotopy/fundamental_group): prove fundamental group is independent of basepoint in path-connected spaces (#12234) Adds definition of fundamental group and proves fundamental group independent of basepoint choice in path-connected spaces. Co-authored-by: Praneeth Kolichala <praneeth.kolichala@gmail.com>