OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node0 line 7
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node0_check line 9
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node0_eval line 12
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node1 line 17
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node1_check line 19
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node1_eval line 22
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node2 line 27
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node2_check line 29
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node2_eval line 32
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node3 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node3_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node3_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node4 line 48
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node4_check line 50
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node4_eval line 53
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node5 line 58
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node5_check line 60
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node5_eval line 63
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node6 line 68
20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node6_check line 70
21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node6_eval line 73
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node7 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node7_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node7_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node8 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node8_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node8_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block1.node9 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node9_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node9_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node10 line 109
32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node10_check line 111
33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node10_eval line 114
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node11 line 119
35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node11_check line 121
36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node11_eval line 124
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node12 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node12_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node12_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node13 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node13_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node13_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node14 line 150
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node14_check line 152
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node14_eval line 155
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node15 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node15_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node15_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node16 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node16_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node16_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node17 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node17_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node17_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node18 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node18_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node18_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node19 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node19_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node19_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node20 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node20_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node20_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block1.node21 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node21_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node21_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node22 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node22_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node22_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node23 line 243
71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node23_check line 245
72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node23_eval line 248
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node24 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node24_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node24_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node25 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node25_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node25_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block1.node26 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node26_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node26_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node27 line 284
83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node27_check line 286
84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node27_eval line 289
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node28 line 294
86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node28_check line 296
87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node28_eval line 299
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node29 line 304
89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node29_check line 306
90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node29_eval line 309
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node30 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node30_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node30_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node31 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node31_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node31_eval line 329