OAI/Analysis/MutuallyUnbiased/GramAssembly/Block2Part3.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block2.node96 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node96_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node96_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block2.node97 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node97_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node97_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block2.node98 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node98_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node98_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block2.node99 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node99_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node99_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block2.node100 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node100_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node100_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block2.node101 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node101_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node101_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block2.node102 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node102_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node102_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block2.node103 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node103_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node103_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block2.node104 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node104_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node104_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block2.node105 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node105_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node105_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block2.node106 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node106_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node106_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block2.node107 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node107_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node107_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block2.node108 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node108_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node108_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block2.node109 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node109_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node109_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part0 line 152
44. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part1 line 154
45. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part2 line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part3 line 158
47. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part4 line 160
48. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part5 line 162
49. def OAI.MUB6.Certificate.GramAssembly.Block2.node110part6 line 164
50. def OAI.MUB6.Certificate.GramAssembly.Block2.node110 line 166
51. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node110_check line 168
52. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node110_eval line 171
53. def OAI.MUB6.Certificate.GramAssembly.Block2.node111 line 175
54. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node111_check line 177
55. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node111_eval line 180
56. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part0 line 184
57. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part1 line 186
58. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part2 line 188
59. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part3 line 190
60. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part4 line 192
61. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part5 line 194
62. def OAI.MUB6.Certificate.GramAssembly.Block2.node112part6 line 196
63. def OAI.MUB6.Certificate.GramAssembly.Block2.node112 line 198
64. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node112_check line 200
65. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node112_eval line 203
66. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part0 line 208
67. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part1 line 210
68. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part2 line 212
69. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part3 line 214
70. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part4 line 216
71. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part5 line 218
72. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part6 line 220
73. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part7 line 222
74. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part8 line 224
75. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part9 line 226
76. def OAI.MUB6.Certificate.GramAssembly.Block2.node113part10 line 228
77. def OAI.MUB6.Certificate.GramAssembly.Block2.node113 line 230
78. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node113_check line 232
79. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node113_eval line 235
80. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part0 line 240
81. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part1 line 242
82. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part2 line 244
83. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part3 line 246
84. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part4 line 248
85. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part5 line 250
86. def OAI.MUB6.Certificate.GramAssembly.Block2.node114part6 line 252
87. def OAI.MUB6.Certificate.GramAssembly.Block2.node114 line 254
88. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node114_check line 256
89. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node114_eval line 259
90. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part0 line 263
91. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part1 line 265
92. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part2 line 267
93. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part3 line 269
94. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part4 line 271
95. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part5 line 273
96. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part6 line 275
97. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part7 line 277
98. def OAI.MUB6.Certificate.GramAssembly.Block2.node115part8 line 279
99. def OAI.MUB6.Certificate.GramAssembly.Block2.node115 line 281
100. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node115_check line 283
101. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node115_eval line 286
102. def OAI.MUB6.Certificate.GramAssembly.Block2.node116 line 291
103. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node116_check line 293
104. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node116_eval line 296
105. def OAI.MUB6.Certificate.GramAssembly.Block2.node117 line 300
106. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node117_check line 302
107. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node117_eval line 305
108. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part0 line 310
109. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part1 line 312
110. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part2 line 314
111. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part3 line 316
112. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part4 line 318
113. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part5 line 320
114. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part6 line 322
115. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part7 line 324
116. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part8 line 326
117. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part9 line 328
118. def OAI.MUB6.Certificate.GramAssembly.Block2.node118part10 line 330
119. def OAI.MUB6.Certificate.GramAssembly.Block2.node118 line 332
120. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node118_check line 334
121. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node118_eval line 337
122. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part0 line 342
123. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part1 line 344
124. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part2 line 346
125. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part3 line 348
126. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part4 line 350
127. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part5 line 352
128. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part6 line 354
129. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part7 line 356
130. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part8 line 358
131. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part9 line 360
132. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part10 line 362
133. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part11 line 364
134. def OAI.MUB6.Certificate.GramAssembly.Block2.node119part12 line 366
135. def OAI.MUB6.Certificate.GramAssembly.Block2.node119 line 368
136. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node119_check line 370
137. theorem OAI.MUB6.Certificate.GramAssembly.Block2.node119_eval line 373