OAI/GroupTheory/SimpleAmenable/Simplicial/StageMonoidal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.muEval line 13
2. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.muEval_inl line 15
3. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.muEval_inr line 18
4. def OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.epsEval line 21
5. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.mu_assoc line 23
6. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.eps_left line 50
7. lemma OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.eps_right line 64
8. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.evaluationMonoidal line 78
9. instance OAI.SimpleAmenable.PolygonObject.LabelledStage.UniformObject.evaluationBraided line 87