OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row24.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_0 line 13
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_0 line 15
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_0 line 19
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_0 line 29
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_1 line 36
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_1 line 38
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_1 line 42
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_1 line 52
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_2 line 59
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_2 line 61
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_2 line 65
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_2 line 75
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_3 line 82
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_3 line 84
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_3 line 88
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_3 line 98
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_4 line 105
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_4 line 107
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_4 line 111
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_4 line 121
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_5 line 128
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_5 line 130
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_5 line 134
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_5 line 144
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_6 line 151
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_6 line 153
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_6 line 157
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_6 line 167
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_7 line 174
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_7 line 176
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_7 line 180
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_7 line 190
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_8 line 197
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_8 line 199
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_8 line 203
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_8 line 213
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_9 line 220
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_9 line 222
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_9 line 226
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_9 line 236
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_10 line 243
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_10 line 245
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_10 line 249
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_10 line 259
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_11 line 266
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_11 line 268
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_11 line 272
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_11 line 282
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_12 line 289
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_12 line 291
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_12 line 295
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_12 line 305
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_13 line 312
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_13 line 314
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_13 line 318
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_13 line 328
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_14 line 335
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_14 line 337
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_14 line 341
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_14 line 351
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_15 line 358
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_15 line 360
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_15 line 364
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_15 line 374
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_16 line 381
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_16 line 383
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_16 line 387
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_16 line 397
69. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_17 line 404
70. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_17 line 406
71. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_17 line 410
72. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_17 line 420
73. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_18 line 427
74. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_18 line 429
75. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_18 line 433
76. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_18 line 443
77. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_19 line 450
78. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_19 line 452
79. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_19 line 456
80. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_19 line 466
81. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_20 line 473
82. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_20 line 475
83. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_20 line 479
84. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_20 line 489
85. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_21 line 496
86. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_21 line 498
87. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_21 line 502
88. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_21 line 512
89. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_22 line 519
90. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_22 line 521
91. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_22 line 525
92. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_22 line 535
93. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_23 line 542
94. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_23 line 544
95. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_23 line 548
96. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_23 line 558
97. def OAI.MUB6.Certificate.GramEntries.Block3.rows24_24 line 565
98. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck24_24 line 567
99. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound24_24 line 571
100. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval24_24 line 581