OAI/GroupTheory/SimpleAmenable/Configurations/TrajectoryCoordinates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SimpleAmenable.PolygonObject.LabelledStage.RankTwo line 15
2. def OAI.SimpleAmenable.PolygonObject.LabelledStage.negativeProjection line 16
3. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.negativeProjection_add line 18
4. def OAI.SimpleAmenable.PolygonObject.LabelledStage.signedLabelEquiv line 24
5. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.signedLabelEquiv_apply line 26
6. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.signedLabel_zero_face line 28
7. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.signedLabel_succ_face line 34
8. def OAI.SimpleAmenable.PolygonObject.LabelledStage.chainCoordinates line 40
9. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.chainCoordinates_single line 44
10. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.chainCoordinates_zero_face line 48
11. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.chainCoordinates_succ_face line 57