OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part7.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node224 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node224_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node224_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node225 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node225_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node225_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node226 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node226_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node226_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node227 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node227_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node227_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node228 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node228_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node228_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node229 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node229_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node229_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node230 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node230_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node230_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node231 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node231_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node231_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node232 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node232_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node232_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node233 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node233_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node233_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node234 line 109
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node234_check line 111
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node234_eval line 114
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node235 line 119
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node235_check line 121
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node235_eval line 124
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node236 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node236_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node236_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node237 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node237_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node237_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node238 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node238_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node238_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node239 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node239_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node239_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node240 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node240_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node240_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node241 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node241_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node241_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node242 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node242_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node242_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node243 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node243_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node243_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node244 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node244_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node244_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node245 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node245_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node245_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node246 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node246_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node246_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node247 line 242
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node247_check line 244
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node247_eval line 247
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node248 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node248_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node248_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node249 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node249_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node249_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node250 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node250_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node250_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node251 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node251_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node251_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node252 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node252_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node252_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node253 line 303
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node253_check line 305
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node253_eval line 308
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node254 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node254_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node254_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node255 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node255_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node255_eval line 329