OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part13.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node416 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node416_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node416_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node417 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node417_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node417_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node418 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node418_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node418_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node419 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node419_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node419_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node420 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node420_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node420_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node421 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node421_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node421_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node422 line 70
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node422_check line 72
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node422_eval line 75
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node423 line 81
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node423_check line 83
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node423_eval line 86
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node424 line 91
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node424_check line 93
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node424_eval line 96
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node425 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node425_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node425_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node426 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node426_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node426_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node427 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node427_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node427_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node428 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node428_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node428_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node429 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node429_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node429_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node430 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node430_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node430_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node431 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node431_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node431_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node432 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node432_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node432_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node433 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node433_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node433_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node434 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node434_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node434_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node435 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node435_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node435_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node436 line 213
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node436_check line 215
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node436_eval line 218
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node437 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node437_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node437_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node438 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node438_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node438_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node439 line 243
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node439_check line 245
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node439_eval line 248
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node440 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node440_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node440_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node441 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node441_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node441_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node442 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node442_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node442_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node443 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node443_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node443_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node444 line 294
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node444_check line 296
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node444_eval line 299
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node445 line 304
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node445_check line 306
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node445_eval line 309
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node446 line 315
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node446_check line 317
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node446_eval line 320
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node447 line 325
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node447_check line 327
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node447_eval line 330