OAI/Combinatorics/SumProduct/Alignment/IntegerArrays02.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SourceIntegerArrays.source_global_literal_array_faces line 30
2. def OAI.SourceIntegerArrays.cubeVertex line 184
3. def OAI.SourceIntegerArrays.cubePattern line 186
4. abbrev OAI.SourceIntegerArrays.CubeIndex line 189
5. abbrev OAI.SourceIntegerArrays.DG line 190
6. abbrev OAI.SourceIntegerArrays.Dn line 191
7. abbrev OAI.SourceIntegerArrays.Dc line 194
8. abbrev OAI.SourceIntegerArrays.Dhsk line 198
9. abbrev OAI.SourceIntegerArrays.DA line 202
10. abbrev OAI.SourceIntegerArrays.Dw line 206
11. abbrev OAI.SourceIntegerArrays.DhA line 210
12. abbrev OAI.SourceIntegerArrays.Dhw line 214
13. abbrev OAI.SourceIntegerArrays.DΓ line 218
14. abbrev OAI.SourceIntegerArrays.CSpace line 220
15. abbrev OAI.SourceIntegerArrays.CLattice line 221
16. abbrev OAI.SourceIntegerArrays.DCspace line 222
17. abbrev OAI.SourceIntegerArrays.DClattice line 223
18. lemma OAI.SourceIntegerArrays.cubePattern_dot line 225
19. def OAI.SourceIntegerArrays.cubeProjection line 231
20. lemma OAI.SourceIntegerArrays.cubeProjection_mk line 245
21. lemma OAI.SourceIntegerArrays.cubeProjection_face line 250
22. lemma OAI.SourceIntegerArrays.cubeProjection_literal line 277
23. theorem OAI.SourceIntegerArrays.literal_cube_interpretation line 295