OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part20.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node640 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node640_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node640_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node641 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node641_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node641_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node642 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node642_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node642_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node643 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node643_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node643_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node644 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node644_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node644_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node645 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node645_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node645_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node646 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node646_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node646_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node647 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node647_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node647_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node648 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node648_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node648_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node649 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node649_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node649_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node650 line 109
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node650_check line 111
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node650_eval line 114
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node651 line 119
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node651_check line 121
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node651_eval line 124
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node652 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node652_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node652_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node653 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node653_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node653_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node654 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node654_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node654_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node655 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node655_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node655_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node656 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node656_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node656_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node657 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node657_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node657_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node658 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node658_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node658_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node659 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node659_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node659_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node660 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node660_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node660_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node661 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node661_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node661_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node662 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node662_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node662_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node663 line 242
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node663_check line 244
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node663_eval line 247
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node664 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node664_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node664_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node665 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node665_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node665_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node666 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node666_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node666_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node667 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node667_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node667_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node668 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node668_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node668_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node669 line 303
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node669_check line 305
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node669_eval line 308
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node670 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node670_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node670_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node671 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node671_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node671_eval line 329