OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part8.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node256 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node256_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node256_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node257 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node257_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node257_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node258 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node258_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node258_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node259 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node259_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node259_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node260 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node260_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node260_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node261 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node261_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node261_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node262 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node262_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node262_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node263 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node263_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node263_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node264 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node264_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node264_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node265 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node265_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node265_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node266 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node266_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node266_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node267 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node267_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node267_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node268 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node268_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node268_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node269 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node269_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node269_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node270 line 153
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node270_check line 155
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node270_eval line 158
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node271 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node271_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node271_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node272 line 173
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node272_check line 175
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node272_eval line 178
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node273 line 183
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node273_check line 185
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node273_eval line 188
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node274 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node274_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node274_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node275 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node275_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node275_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node276 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node276_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node276_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node277 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node277_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node277_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node278 line 234
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node278_check line 236
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node278_eval line 239
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node279 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node279_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node279_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node280 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node280_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node280_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node281 line 266
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node281_check line 268
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node281_eval line 271
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node282 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node282_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node282_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node283 line 286
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node283_check line 288
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node283_eval line 291
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node284 line 296
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node284_check line 298
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node284_eval line 301
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node285 line 306
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node285_check line 308
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node285_eval line 311
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node286 line 317
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node286_check line 319
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node286_eval line 322
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node287 line 327
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node287_check line 329
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node287_eval line 332