OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part12.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node384 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node384_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node384_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node385 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node385_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node385_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node386 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node386_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node386_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node387 line 38
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node387_check line 40
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node387_eval line 43
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node388 line 48
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node388_check line 50
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node388_eval line 53
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node389 line 58
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node389_check line 60
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node389_eval line 63
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node390 line 68
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node390_check line 70
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node390_eval line 73
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node391 line 78
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node391_check line 80
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node391_eval line 83
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node392 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node392_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node392_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node393 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node393_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node393_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node394 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node394_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node394_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node395 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node395_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node395_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node396 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node396_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node396_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node397 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node397_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node397_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node398 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node398_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node398_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node399 line 161
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node399_check line 163
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node399_eval line 166
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node400 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node400_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node400_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node401 line 181
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node401_check line 183
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node401_eval line 186
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node402 line 191
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node402_check line 193
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node402_eval line 196
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node403 line 201
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node403_check line 203
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node403_eval line 206
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node404 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node404_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node404_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node405 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node405_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node405_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node406 line 232
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node406_check line 234
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node406_eval line 237
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node407 line 242
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node407_check line 244
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node407_eval line 247
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node408 line 252
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node408_check line 254
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node408_eval line 257
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node409 line 262
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node409_check line 264
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node409_eval line 267
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node410 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node410_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node410_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node411 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node411_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node411_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node412 line 293
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node412_check line 295
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node412_eval line 298
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node413 line 303
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node413_check line 305
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node413_eval line 308
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node414 line 313
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node414_check line 315
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node414_eval line 318
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node415 line 323
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node415_check line 325
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node415_eval line 328