OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part4.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node128 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node128_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node128_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node129 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node129_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node129_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node130 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node130_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node130_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node131 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node131_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node131_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node132 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node132_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node132_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node133 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node133_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node133_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node134 line 71
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node134_check line 73
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node134_eval line 76
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node135 line 81
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node135_check line 83
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node135_eval line 86
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node136 line 91
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node136_check line 93
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node136_eval line 96
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node137 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node137_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node137_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node138 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node138_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node138_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node139 line 122
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node139_check line 124
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node139_eval line 127
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node140 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node140_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node140_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node141 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node141_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node141_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node142 line 153
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node142_check line 155
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node142_eval line 158
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node143 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node143_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node143_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node144 line 174
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node144_check line 176
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node144_eval line 179
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node145 line 184
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node145_check line 186
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node145_eval line 189
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node146 line 194
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node146_check line 196
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node146_eval line 199
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node147 line 204
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node147_check line 206
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node147_eval line 209
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node148 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node148_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node148_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node149 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node149_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node149_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node150 line 235
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node150_check line 237
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node150_eval line 240
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node151 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node151_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node151_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node152 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node152_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node152_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node153 line 266
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node153_check line 268
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node153_eval line 271
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node154 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node154_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node154_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node155 line 287
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node155_check line 289
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node155_eval line 292
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node156 line 297
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node156_check line 299
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node156_eval line 302
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node157 line 307
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node157_check line 309
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node157_eval line 312
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node158 line 317
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node158_check line 319
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node158_eval line 322
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node159 line 327
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node159_check line 329
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node159_eval line 332