OAI/Geometry/HyperbolicGroups/PictureRestrict.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HyperbolicObstruction.PictureSwitch.invariant_of_sameCycleline 18 - lemma
OAI.HyperbolicObstruction.PictureSwitch.cycles_subtype_splitline 24