OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part14.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node448 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node448_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node448_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node449 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node449_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node449_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node450 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node450_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node450_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node451 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node451_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node451_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node452 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node452_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node452_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node453 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node453_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node453_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node454 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node454_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node454_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node455 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node455_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node455_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node456 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node456_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node456_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node457 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node457_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node457_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node458 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node458_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node458_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node459 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node459_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node459_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node460 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node460_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node460_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node461 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node461_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node461_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node462 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node462_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node462_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node463 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node463_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node463_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node464 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node464_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node464_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node465 line 181
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node465_check line 183
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node465_eval line 186
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node466 line 191
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node466_check line 193
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node466_eval line 196
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node467 line 201
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node467_check line 203
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node467_eval line 206
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node468 line 211
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node468_check line 213
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node468_eval line 216
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node469 line 221
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node469_check line 223
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node469_eval line 226
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node470 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node470_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node470_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node471 line 242
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node471_check line 244
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node471_eval line 247
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node472 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node472_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node472_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node473 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node473_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node473_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node474 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node474_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node474_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node475 line 284
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node475_check line 286
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node475_eval line 289
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node476 line 294
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node476_check line 296
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node476_eval line 299
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node477 line 304
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node477_check line 306
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node477_eval line 309
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node478 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node478_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node478_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node479 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node479_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node479_eval line 329