OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PolygonComponentCompletion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SimpleAmenable.PolygonObject.Component line 18
2. abbrev OAI.SimpleAmenable.PolygonObject.component line 19
3. theorem OAI.SimpleAmenable.PolygonObject.component_sum line 21
4. theorem OAI.SimpleAmenable.PolygonObject.sum_standard line 25
5. theorem OAI.SimpleAmenable.PolygonObject.component_standard_zero line 31
6. theorem OAI.SimpleAmenable.PolygonObject.component_standard_add line 40
7. theorem OAI.SimpleAmenable.PolygonObject.component_standard_pow line 44
8. theorem OAI.SimpleAmenable.PolygonObject.component_complement line 50
9. abbrev OAI.SimpleAmenable.PolygonObject.CompletedComponent line 55
10. abbrev OAI.SimpleAmenable.PolygonObject.completedComponent line 56
11. theorem OAI.SimpleAmenable.PolygonObject.completion_eq_iff line 59
12. theorem OAI.SimpleAmenable.PolygonObject.neutral_component_eventually_standard line 81