OAI/Geometry/HyperbolicGroups/Main.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

All existential clauses use the same selected finite complex and the same actual fundamental group.

  1. theorem OAI.HyperbolicObstruction.main line 15

    Distinct definitions of this name: ComparatorChallenges/HyperbolicObstruction.lean:154 (same statement text; different proof or body). Qualify references as OAI.HyperbolicObstruction.main@path.