OAI/Analysis/MutuallyUnbiased/GramAssembly/Block2Part1.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block2.node32 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node32_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node32_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block2.node33 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node33_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node33_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block2.node34 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node34_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node34_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block2.node35 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node35_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node35_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block2.node36 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node36_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node36_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block2.node37 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node37_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node37_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block2.node38 line 71
20. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node38_check line 73
21. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node38_eval line 76
22. def OAI.MUB6.Certificate.GramAssembly.Block2.node39 line 81
23. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node39_check line 83
24. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node39_eval line 86
25. def OAI.MUB6.Certificate.GramAssembly.Block2.node40 line 91
26. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node40_check line 93
27. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node40_eval line 96
28. def OAI.MUB6.Certificate.GramAssembly.Block2.node41 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node41_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node41_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block2.node42 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node42_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node42_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block2.node43 line 122
35. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node43_check line 124
36. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node43_eval line 127
37. def OAI.MUB6.Certificate.GramAssembly.Block2.node44 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node44_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node44_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block2.node45 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node45_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node45_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block2.node46 line 153
44. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node46_check line 155
45. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node46_eval line 158
46. def OAI.MUB6.Certificate.GramAssembly.Block2.node47 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node47_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node47_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block2.node48 line 174
50. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node48_check line 176
51. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node48_eval line 179
52. def OAI.MUB6.Certificate.GramAssembly.Block2.node49 line 184
53. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node49_check line 186
54. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node49_eval line 189
55. def OAI.MUB6.Certificate.GramAssembly.Block2.node50 line 194
56. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node50_check line 196
57. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node50_eval line 199
58. def OAI.MUB6.Certificate.GramAssembly.Block2.node51 line 204
59. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node51_check line 206
60. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node51_eval line 209
61. def OAI.MUB6.Certificate.GramAssembly.Block2.node52 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node52_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node52_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block2.node53 line 225
65. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node53_check line 227
66. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node53_eval line 230
67. def OAI.MUB6.Certificate.GramAssembly.Block2.node54 line 235
68. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node54_check line 237
69. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node54_eval line 240
70. def OAI.MUB6.Certificate.GramAssembly.Block2.node55 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node55_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node55_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block2.node56 line 256
74. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node56_check line 258
75. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node56_eval line 261
76. def OAI.MUB6.Certificate.GramAssembly.Block2.node57 line 266
77. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node57_check line 268
78. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node57_eval line 271
79. def OAI.MUB6.Certificate.GramAssembly.Block2.node58 line 277
80. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node58_check line 279
81. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node58_eval line 282
82. def OAI.MUB6.Certificate.GramAssembly.Block2.node59 line 287
83. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node59_check line 289
84. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node59_eval line 292
85. def OAI.MUB6.Certificate.GramAssembly.Block2.node60 line 297
86. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node60_check line 299
87. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node60_eval line 302
88. def OAI.MUB6.Certificate.GramAssembly.Block2.node61 line 307
89. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node61_check line 309
90. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node61_eval line 312
91. def OAI.MUB6.Certificate.GramAssembly.Block2.node62 line 317
92. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node62_check line 319
93. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node62_eval line 322
94. def OAI.MUB6.Certificate.GramAssembly.Block2.node63 line 328
95. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node63_check line 330
96. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node63_eval line 333