OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part12.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block1.node384 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node384_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node384_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block1.node385 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node385_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node385_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block1.node386 line 28
8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node386_check line 30
9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node386_eval line 33
10. def OAI.MUB6.Certificate.GramAssembly.Block1.node387 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node387_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node387_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block1.node388 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node388_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node388_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block1.node389 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node389_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node389_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block1.node390 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node390_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node390_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block1.node391 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node391_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node391_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block1.node392 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node392_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node392_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block1.node393 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node393_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node393_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block1.node394 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node394_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node394_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block1.node395 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node395_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node395_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block1.node396 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node396_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node396_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block1.node397 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node397_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node397_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block1.node398 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node398_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node398_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block1.node399 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node399_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node399_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block1.node400 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node400_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node400_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block1.node401 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node401_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node401_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block1.node402 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node402_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node402_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block1.node403 line 203
59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node403_check line 205
60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node403_eval line 208
61. def OAI.MUB6.Certificate.GramAssembly.Block1.node404 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node404_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node404_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block1.node405 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node405_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node405_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block1.node406 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node406_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node406_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block1.node407 line 244
71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node407_check line 246
72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node407_eval line 249
73. def OAI.MUB6.Certificate.GramAssembly.Block1.node408 line 254
74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node408_check line 256
75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node408_eval line 259
76. def OAI.MUB6.Certificate.GramAssembly.Block1.node409 line 264
77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node409_check line 266
78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node409_eval line 269
79. def OAI.MUB6.Certificate.GramAssembly.Block1.node410 line 274
80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node410_check line 276
81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node410_eval line 279
82. def OAI.MUB6.Certificate.GramAssembly.Block1.node411 line 284
83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node411_check line 286
84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node411_eval line 289
85. def OAI.MUB6.Certificate.GramAssembly.Block1.node412 line 295
86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node412_check line 297
87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node412_eval line 300
88. def OAI.MUB6.Certificate.GramAssembly.Block1.node413 line 305
89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node413_check line 307
90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node413_eval line 310
91. def OAI.MUB6.Certificate.GramAssembly.Block1.node414 line 315
92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node414_check line 317
93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node414_eval line 320
94. def OAI.MUB6.Certificate.GramAssembly.Block1.node415 line 326
95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node415_check line 328
96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node415_eval line 331