OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part7.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node224 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node224_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node224_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node225 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node225_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node225_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node226 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node226_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node226_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node227 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node227_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node227_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node228 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node228_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node228_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node229 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node229_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node229_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node230 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node230_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node230_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node231 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node231_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node231_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node232 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node232_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node232_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block1.node233 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node233_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node233_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node234 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node234_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node234_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node235 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node235_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node235_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node236 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node236_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node236_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node237 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node237_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node237_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node238 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node238_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node238_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node239 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node239_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node239_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node240 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node240_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node240_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node241 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node241_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node241_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node242 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node242_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node242_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node243 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node243_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node243_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node244 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node244_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node244_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block1.node245 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node245_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node245_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node246 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node246_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node246_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node247 line 244
71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node247_check line 246
72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node247_eval line 249
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node248 line 254
74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node248_check line 256
75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node248_eval line 259
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node249 line 264
77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node249_check line 266
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node249_eval line 269
79. def OAI.MUB6.Certificate.GramAssembly.Block1.node250 line 274
80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node250_check line 276
81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node250_eval line 279
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node251 line 284
83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node251_check line 286
84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node251_eval line 289
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node252 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node252_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node252_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node253 line 305
89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node253_check line 307
90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node253_eval line 310
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node254 line 315
92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node254_check line 317
93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node254_eval line 320
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node255 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node255_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node255_eval line 331