Computations and applications dependency map

Parent map · Full theorem DAG

This map shows the container's direct articles. Nested containers are collapsed and clickable; dependency edges are rolled up from their leaves. What the colours mean

in mathlib6Upstreamed into Mathlib.fully proved116Proved, and every prerequisite is fully proved too.ready to state2Prerequisites are stated, so this can be written down.planned5Described in the blueprint only.

graph LR n0["Degree foundations and applications<br/><small>16 items · 16 fully proved</small>"]:::scope n1["Local degree and the sum over a finite fiber<br/><small>20 items · 13 fully proved · 2 ready to state · 5 planned</small>"]:::scope n2["Local homology and invariance of dimension<br/><small>4 items · 4 fully proved</small>"]:::scope n3["Mayer–Vietoris sequences<br/><small>6 items · 6 fully proved</small>"]:::scope n4["Post-excision applications<br/><small>28 items · 28 fully proved</small>"]:::scope n5["Mayer–Vietoris transport, sphere homology, and Brouwer<br/><small>16 items · 16 fully proved</small>"]:::scope n6["External chapter: The fundamental group<br/><small>8 items · 8 fully proved</small>"]:::boundary n7["External chapter: Homology<br/><small>31 items · 6 in mathlib · 25 fully proved</small>"]:::boundary n6 -->|2| n4 n6 -. 6 .-> n4 n6 --> n5 n7 --> n0 n7 -->|2| n1 n7 -.-> n1 n7 -->|2| n2 n7 -.-> n2 n7 -->|7| n3 n7 -. 3 .-> n3 n7 -->|22| n4 n7 -. 19 .-> n4 n7 -->|7| n5 n7 -. 8 .-> n5 n0 -->|4| n1 n2 -->|3| n1 n3 -->|2| n5 n4 -->|4| n0 n4 -->|3| n1 n4 -.-> n1 n5 -. 2 .-> n0 n5 -. 4 .-> n2 n5 -. 2 .-> n4 click n0 "computations-and-applications/degree.html" "Degree foundations and applications — 16 items · 16 fully proved" click n1 "computations-and-applications/local-degree.html" "Local degree and the sum over a finite fiber — 20 items · 13 fully proved · 2 ready to state · 5 planned" click n2 "computations-and-applications/local-homology-and-dimension.html" "Local homology and invariance of dimension — 4 items · 4 fully proved" click n3 "computations-and-applications/mayer-vietoris.html" "Mayer–Vietoris sequences — 6 items · 6 fully proved" click n4 "computations-and-applications/post-excision-applications.html" "Post-excision applications — 28 items · 28 fully proved" click n5 "computations-and-applications/sphere-homology.html" "Mayer–Vietoris transport, sphere homology, and Brouwer — 16 items · 16 fully proved" click n6 "../../chapters/fundamental-group.html" "The fundamental group — 8 items · 8 fully proved" click n7 "../../chapters/homology.html" "Homology — 31 items · 6 in mathlib · 25 fully proved"