The fundamental group dependency map

Project map · Full theorem DAG · Open textbook chapter

This map contains the 118 decomposed items in this chapter. Dashed chapter boxes stand for external prerequisites or dependents.

in mathlib8Upstreamed into Mathlib.fully proved118Proved, and every prerequisite is fully proved too.

graph LR n0["Basic constructions<br/><small>22 items · 4 in mathlib · 18 fully proved</small>"]:::scope n1["Covering spaces<br/><small>32 items · 4 in mathlib · 28 fully proved</small>"]:::scope n2["Van Kampen's theorem<br/><small>64 items · 64 fully proved</small>"]:::scope n3["External chapter: Appendix<br/><small>2 items · 2 fully proved</small>"]:::boundary n4["External chapter: Homology<br/><small>6 items · 6 fully proved</small>"]:::boundary n3 -. 4 .-> n2 n0 -->|6| n2 n0 -. 4 .-> n2 n2 -->|3| n4 n2 -. 6 .-> n4 click n0 "../scopes/fundamental-group/basic-constructions.html" "Basic constructions — 22 items · 4 in mathlib · 18 fully proved" click n1 "../scopes/fundamental-group/covering-spaces.html" "Covering spaces — 32 items · 4 in mathlib · 28 fully proved" click n2 "../scopes/fundamental-group/van-kampen.html" "Van Kampen's theorem — 64 items · 64 fully proved" click n3 "appendix.html" "Appendix — 2 items · 2 fully proved" click n4 "homology.html" "Homology — 6 items · 6 fully proved"