OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part7.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node224 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node224_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node224_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node225 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node225_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node225_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node226 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node226_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node226_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node227 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node227_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node227_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node228 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node228_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node228_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node229 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node229_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node229_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node230 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node230_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node230_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node231 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node231_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node231_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node232 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node232_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node232_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node233 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node233_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node233_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node234 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node234_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node234_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node235 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node235_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node235_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node236 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node236_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node236_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node237 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node237_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node237_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node238 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node238_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node238_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node239 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node239_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node239_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node240 line 173
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node240_check line 175
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node240_eval line 178
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node241 line 183
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node241_check line 185
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node241_eval line 188
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node242 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node242_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node242_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node243 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node243_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node243_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node244 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node244_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node244_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node245 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node245_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node245_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node246 line 234
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node246_check line 236
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node246_eval line 239
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node247 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node247_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node247_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node248 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node248_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node248_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node249 line 266
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node249_check line 268
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node249_eval line 271
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node250 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node250_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node250_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node251 line 286
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node251_check line 288
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node251_eval line 291
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node252 line 296
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node252_check line 298
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node252_eval line 301
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node253 line 306
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node253_check line 308
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node253_eval line 311
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node254 line 316
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node254_check line 318
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node254_eval line 321
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node255 line 327
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node255_check line 329
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node255_eval line 332