OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part6.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node192 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node192_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node192_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node193 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node193_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node193_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node194 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node194_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node194_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node195 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node195_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node195_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node196 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node196_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node196_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node197 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node197_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node197_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node198 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node198_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node198_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node199 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node199_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node199_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node200 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node200_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node200_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node201 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node201_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node201_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node202 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node202_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node202_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node203 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node203_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node203_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node204 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node204_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node204_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node205 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node205_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node205_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node206 line 150
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node206_check line 152
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node206_eval line 155
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node207 line 160
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node207_check line 162
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node207_eval line 165
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node208 line 170
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node208_check line 172
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node208_eval line 175
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node209 line 180
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node209_check line 182
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node209_eval line 185
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node210 line 191
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node210_check line 193
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node210_eval line 196
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node211 line 201
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node211_check line 203
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node211_eval line 206
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node212 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node212_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node212_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node213 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node213_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node213_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node214 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node214_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node214_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node215 line 243
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node215_check line 245
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node215_eval line 248
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node216 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node216_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node216_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node217 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node217_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node217_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node218 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node218_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node218_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node219 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node219_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node219_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node220 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node220_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node220_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node221 line 303
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node221_check line 305
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node221_eval line 308
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node222 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node222_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node222_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node223 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node223_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node223_eval line 329