OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part3.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node96 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node96_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node96_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node97 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node97_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node97_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node98 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node98_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node98_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node99 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node99_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node99_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node100 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node100_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node100_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node101 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node101_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node101_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node102 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node102_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node102_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node103 line 80
23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node103_check line 82
24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node103_eval line 85
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node104 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node104_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node104_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block1.node105 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node105_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node105_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node106 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node106_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node106_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node107 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node107_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node107_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node108 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node108_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node108_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node109 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node109_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node109_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node110 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node110_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node110_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node111 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node111_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node111_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node112 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node112_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node112_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node113 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node113_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node113_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node114 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node114_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node114_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node115 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node115_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node115_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node116 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node116_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node116_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block1.node117 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node117_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node117_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node118 line 234
68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node118_check line 236
69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node118_eval line 239
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node119 line 244
71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node119_check line 246
72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node119_eval line 249
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node120 line 254
74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node120_check line 256
75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node120_eval line 259
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node121 line 264
77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node121_check line 266
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node121_eval line 269
79. def OAI.MUB6.Certificate.GramAssembly.Block1.node122 line 274
80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node122_check line 276
81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node122_eval line 279
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node123 line 285
83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node123_check line 287
84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node123_eval line 290
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node124 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node124_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node124_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node125 line 305
89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node125_check line 307
90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node125_eval line 310
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node126 line 315
92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node126_check line 317
93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node126_eval line 320
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node127 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node127_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node127_eval line 331