OAI/SetTheory/PartitionPrinciple/Geometry/DecodedGroundGroups.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroupCode.mul line 13
2. def OAI.PartitionPilot.Forcing.GroupCode.inv line 17
3. def OAI.PartitionPilot.Forcing.GroupCode.one line 20
4. theorem OAI.PartitionPilot.Forcing.GroupCode.raw_one line 22
5. theorem OAI.PartitionPilot.Forcing.GroupCode.mul_mem line 24
6. theorem OAI.PartitionPilot.Forcing.GroupCode.inv_mem line 29
7. theorem OAI.PartitionPilot.Forcing.GroupCode.mul_eq_iff line 33
8. theorem OAI.PartitionPilot.Forcing.GroupCode.decoded_one_mul line 38
9. theorem OAI.PartitionPilot.Forcing.GroupCode.decoded_mul_one line 43
10. theorem OAI.PartitionPilot.Forcing.GroupCode.decoded_inv_mul line 48
11. theorem OAI.PartitionPilot.Forcing.GroupCode.decoded_mul_assoc line 53
12. def OAI.PartitionPilot.Forcing.GroupCode.toGroup line 62
13. theorem OAI.PartitionPilot.Forcing.GroupCode.multiplication_graph_eq line 71
14. theorem OAI.PartitionPilot.Forcing.GroupCode.inverse_graph_eq line 79
15. theorem OAI.PartitionPilot.Forcing.GroupCode.identity_code_eq line 85
16. def OAI.PartitionPilot.Forcing.TransitiveGround.decodedGroup line 97
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.decoded_group_graphs_mem line 103