OAI/GroupTheory/SimpleAmenable/Configurations/LabelledStringEquiv.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SimpleAmenable.PolygonObject.Labelled.initialCoreline 14 - lemma
OAI.SimpleAmenable.PolygonObject.Labelled.initialCore_unitline 16 - lemma
OAI.SimpleAmenable.PolygonObject.Labelled.initialCore_tensorline 19 - def
OAI.SimpleAmenable.PolygonObject.Labelled.stringsCoreline 30 - instance
OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 72)line 72 - instance
OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 73)line 73 - lemma
OAI.SimpleAmenable.PolygonObject.Labelled.tripleBar_homology_isIsoline 91 - theorem
OAI.SimpleAmenable.PolygonObject.LabelledStage.exists_common_stageline 106