Mathlib v3 is deprecated. Go to Mathlib v4

Def fundamental_groupoid.from_top

Modification history

2022-02-27 04:07
src/topology/homotopy/fundamental_groupoid.lean
feat(category_theory/category/Groupoid): Add coercion to sort (#12324) …
Modified fundamental_groupoid.from_topView on Github →
2022-02-02 07:21
src/topology/homotopy/fundamental_groupoid.lean
feat(topology/homotopy): Fundamental groupoid preserves products (#11459)
Added fundamental_groupoid.from_topView on Github →