Home

Goal: Formalizing GGT and prove Stalling's theorem

If possible: get things merged in mathlib, but this may be complicated (needs perfect code).

Out of scope

• (Locally compact) topological groups probably would be too much.

What I need:

• Bass-Serre theory
• Coarse geometry
• Cayley graphs/metrics