OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part2.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node64 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node64_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node64_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node65 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node65_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node65_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node66 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node66_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node66_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node67 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node67_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node67_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node68 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node68_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node68_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node69 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node69_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node69_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node70 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node70_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node70_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node71 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node71_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node71_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node72 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node72_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node72_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block1.node73 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node73_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node73_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node74 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node74_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node74_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node75 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node75_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node75_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node76 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node76_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node76_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node77 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node77_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node77_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node78 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node78_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node78_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node79 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node79_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node79_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node80 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node80_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node80_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node81 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node81_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node81_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node82 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node82_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node82_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node83 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node83_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node83_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node84 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node84_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node84_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block1.node85 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node85_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node85_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node86 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node86_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node86_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node87 line 244
71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node87_check line 246
72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node87_eval line 249
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node88 line 254
74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node88_check line 256
75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node88_eval line 259
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node89 line 264
77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node89_check line 266
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node89_eval line 269
79. def OAI.MUB6.Certificate.GramAssembly.Block1.node90 line 274
80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node90_check line 276
81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node90_eval line 279
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node91 line 284
83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node91_check line 286
84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node91_eval line 289
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node92 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node92_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node92_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node93 line 305
89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node93_check line 307
90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node93_eval line 310
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node94 line 315
92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node94_check line 317
93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node94_eval line 320
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node95 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node95_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node95_eval line 331