OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part10.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node320 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node320_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node320_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node321 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node321_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node321_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node322 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node322_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node322_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node323 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node323_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node323_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node324 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node324_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node324_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node325 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node325_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node325_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node326 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node326_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node326_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node327 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node327_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node327_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node328 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node328_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node328_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block1.node329 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node329_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node329_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node330 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node330_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node330_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node331 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node331_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node331_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node332 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node332_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node332_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node333 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node333_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node333_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node334 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node334_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node334_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node335 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node335_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node335_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node336 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node336_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node336_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node337 line 183
53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node337_check line 185
54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node337_eval line 188
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node338 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node338_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node338_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node339 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node339_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node339_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node340 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node340_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node340_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block1.node341 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node341_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node341_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node342 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node342_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node342_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node343 line 244
71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node343_check line 246
72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node343_eval line 249
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node344 line 254
74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node344_check line 256
75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node344_eval line 259
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node345 line 264
77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node345_check line 266
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node345_eval line 269
79. def OAI.MUB6.Certificate.GramAssembly.Block1.node346 line 274
80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node346_check line 276
81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node346_eval line 279
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node347 line 285
83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node347_check line 287
84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node347_eval line 290
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node348 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node348_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node348_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node349 line 305
89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node349_check line 307
90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node349_eval line 310
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node350 line 315
92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node350_check line 317
93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node350_eval line 320
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node351 line 325
95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node351_check line 327
96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node351_eval line 330