OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part11.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node352 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node352_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node352_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node353 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node353_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node353_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node354 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node354_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node354_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node355 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node355_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node355_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node356 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node356_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node356_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node357 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node357_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node357_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node358 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node358_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node358_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node359 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node359_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node359_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node360 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node360_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node360_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node361 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node361_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node361_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node362 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node362_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node362_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node363 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node363_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node363_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node364 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node364_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node364_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node365 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node365_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node365_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node366 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node366_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node366_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node367 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node367_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node367_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node368 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node368_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node368_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node369 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node369_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node369_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node370 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node370_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node370_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node371 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node371_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node371_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node372 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node372_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node372_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node373 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node373_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node373_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node374 line 234
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node374_check line 236
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node374_eval line 239
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node375 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node375_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node375_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node376 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node376_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node376_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node377 line 265
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node377_check line 267
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node377_eval line 270
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node378 line 275
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node378_check line 277
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node378_eval line 280
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node379 line 285
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node379_check line 287
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node379_eval line 290
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node380 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node380_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node380_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node381 line 306
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node381_check line 308
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node381_eval line 311
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node382 line 316
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node382_check line 318
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node382_eval line 321
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node383 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node383_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node383_eval line 331