OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part18.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node576 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node576_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node576_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node577 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node577_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node577_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node578 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node578_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node578_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node579 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node579_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node579_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node580 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node580_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node580_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node581 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node581_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node581_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node582 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node582_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node582_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node583 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node583_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node583_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node584 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node584_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node584_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node585 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node585_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node585_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node586 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node586_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node586_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node587 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node587_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node587_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node588 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node588_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node588_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node589 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node589_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node589_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node590 line 150
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node590_check line 152
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node590_eval line 155
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node591 line 160
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node591_check line 162
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node591_eval line 165
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node592 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node592_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node592_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node593 line 181
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node593_check line 183
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node593_eval line 186
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node594 line 191
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node594_check line 193
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node594_eval line 196
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node595 line 201
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node595_check line 203
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node595_eval line 206
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node596 line 211
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node596_check line 213
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node596_eval line 216
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node597 line 221
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node597_check line 223
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node597_eval line 226
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node598 line 231
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node598_check line 233
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node598_eval line 236
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node599 line 241
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node599_check line 243
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node599_eval line 246
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node600 line 252
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node600_check line 254
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node600_eval line 257
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node601 line 262
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node601_check line 264
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node601_eval line 267
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node602 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node602_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node602_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node603 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node603_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node603_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node604 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node604_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node604_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node605 line 304
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node605_check line 306
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node605_eval line 309
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node606 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node606_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node606_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node607 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node607_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node607_eval line 329