OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part10.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node320 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node320_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node320_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node321 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node321_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node321_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node322 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node322_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node322_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node323 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node323_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node323_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node324 line 48
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node324_check line 50
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node324_eval line 53
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node325 line 58
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node325_check line 60
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node325_eval line 63
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node326 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node326_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node326_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node327 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node327_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node327_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node328 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node328_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node328_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node329 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node329_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node329_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node330 line 109
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node330_check line 111
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node330_eval line 114
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node331 line 119
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node331_check line 121
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node331_eval line 124
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node332 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node332_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node332_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node333 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node333_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node333_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node334 line 150
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node334_check line 152
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node334_eval line 155
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node335 line 160
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node335_check line 162
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node335_eval line 165
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node336 line 170
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node336_check line 172
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node336_eval line 175
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node337 line 180
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node337_check line 182
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node337_eval line 185
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node338 line 190
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node338_check line 192
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node338_eval line 195
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node339 line 200
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node339_check line 202
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node339_eval line 205
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node340 line 211
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node340_check line 213
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node340_eval line 216
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node341 line 221
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node341_check line 223
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node341_eval line 226
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node342 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node342_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node342_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node343 line 242
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node343_check line 244
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node343_eval line 247
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node344 line 252
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node344_check line 254
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node344_eval line 257
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node345 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node345_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node345_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node346 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node346_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node346_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node347 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node347_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node347_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node348 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node348_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node348_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node349 line 303
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node349_check line 305
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node349_eval line 308
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node350 line 313
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node350_check line 315
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node350_eval line 318
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node351 line 323
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node351_check line 325
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node351_eval line 328