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"