OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part5.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node160 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node160_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node160_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node161 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node161_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node161_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node162 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node162_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node162_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node163 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node163_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node163_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node164 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node164_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node164_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node165 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node165_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node165_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node166 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node166_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node166_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node167 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node167_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node167_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node168 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node168_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node168_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node169 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node169_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node169_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node170 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node170_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node170_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node171 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node171_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node171_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node172 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node172_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node172_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node173 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node173_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node173_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node174 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node174_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node174_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node175 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node175_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node175_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node176 line 173
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node176_check line 175
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node176_eval line 178
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node177 line 183
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node177_check line 185
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node177_eval line 188
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node178 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node178_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node178_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node179 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node179_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node179_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node180 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node180_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node180_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node181 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node181_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node181_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node182 line 234
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node182_check line 236
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node182_eval line 239
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node183 line 244
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node183_check line 246
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node183_eval line 249
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node184 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node184_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node184_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node185 line 265
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node185_check line 267
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node185_eval line 270
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node186 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node186_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node186_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node187 line 286
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node187_check line 288
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node187_eval line 291
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node188 line 296
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node188_check line 298
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node188_eval line 301
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node189 line 306
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node189_check line 308
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node189_eval line 311
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node190 line 316
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node190_check line 318
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node190_eval line 321
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node191 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node191_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node191_eval line 331