OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node0 line 7
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node0_check line 9
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node0_eval line 12
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node1 line 17
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node1_check line 19
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node1_eval line 22
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node2 line 27
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node2_check line 29
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node2_eval line 32
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node3 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node3_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node3_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node4 line 48
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node4_check line 50
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node4_eval line 53
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node5 line 58
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node5_check line 60
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node5_eval line 63
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node6 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node6_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node6_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node7 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node7_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node7_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node8 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node8_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node8_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node9 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node9_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node9_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node10 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node10_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node10_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node11 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node11_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node11_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node12 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node12_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node12_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node13 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node13_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node13_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node14 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node14_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node14_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node15 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node15_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node15_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node16 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node16_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node16_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node17 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node17_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node17_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node18 line 193
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node18_check line 195
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node18_eval line 198
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node19 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node19_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node19_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node20 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node20_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node20_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node21 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node21_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node21_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node22 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node22_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node22_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node23 line 243
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node23_check line 245
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node23_eval line 248
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node24 line 254
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node24_check line 256
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node24_eval line 259
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node25 line 264
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node25_check line 266
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node25_eval line 269
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node26 line 274
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node26_check line 276
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node26_eval line 279
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node27 line 285
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node27_check line 287
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node27_eval line 290
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node28 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node28_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node28_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node29 line 306
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node29_check line 308
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node29_eval line 311
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node30 line 316
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node30_check line 318
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node30_eval line 321
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node31 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node31_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node31_eval line 331