OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part10.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node320 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node320_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node320_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node321 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node321_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node321_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node322 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node322_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node322_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node323 line 40
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node323_check line 42
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node323_eval line 45
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node324 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node324_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node324_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node325 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node325_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node325_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node326 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node326_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node326_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node327 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node327_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node327_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node328 line 91
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node328_check line 93
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node328_eval line 96
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node329 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node329_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node329_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node330 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node330_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node330_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node331 line 122
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node331_check line 124
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node331_eval line 127
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node332 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node332_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node332_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node333 line 143
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node333_check line 145
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node333_eval line 148
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node334 line 153
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node334_check line 155
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node334_eval line 158
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node335 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node335_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node335_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node336 line 173
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node336_check line 175
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node336_eval line 178
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node337 line 183
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node337_check line 185
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node337_eval line 188
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node338 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node338_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node338_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node339 line 204
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node339_check line 206
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node339_eval line 209
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node340 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node340_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node340_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node341 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node341_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node341_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node342 line 235
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node342_check line 237
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node342_eval line 240
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node343 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node343_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node343_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node344 line 256
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node344_check line 258
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node344_eval line 261
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node345 line 266
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node345_check line 268
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node345_eval line 271
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node346 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node346_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node346_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node347 line 286
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node347_check line 288
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node347_eval line 291
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node348 line 296
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node348_check line 298
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node348_eval line 301
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node349 line 307
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node349_check line 309
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node349_eval line 312
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node350 line 317
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node350_check line 319
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node350_eval line 322
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node351 line 327
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node351_check line 329
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node351_eval line 332