OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row25.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_0 line 13
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_0 line 15
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_0 line 19
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_0 line 32
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_1 line 39
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_1 line 41
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_1 line 45
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_1 line 58
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_2 line 65
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_2 line 67
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_2 line 71
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_2 line 84
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_3 line 91
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_3 line 93
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_3 line 97
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_3 line 110
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_4 line 117
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_4 line 119
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_4 line 123
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_4 line 136
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_5 line 143
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_5 line 145
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_5 line 149
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_5 line 162
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_6 line 169
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_6 line 171
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_6 line 175
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_6 line 188
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_7 line 195
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_7 line 197
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_7 line 201
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_7 line 214
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_8 line 221
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_8 line 223
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_8 line 227
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_8 line 240
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_9 line 247
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_9 line 249
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_9 line 253
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_9 line 266
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_10 line 273
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_10 line 275
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_10 line 279
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_10 line 292
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_11 line 299
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_11 line 301
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_11 line 305
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_11 line 318
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_12 line 325
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_12 line 327
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_12 line 331
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_12 line 344
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_13 line 351
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_13 line 353
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_13 line 357
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_13 line 370
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_14 line 377
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_14 line 379
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_14 line 383
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_14 line 396
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_15 line 403
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_15 line 405
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_15 line 409
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_15 line 422
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_16 line 429
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_16 line 431
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_16 line 435
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_16 line 448
69. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_17 line 455
70. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_17 line 457
71. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_17 line 461
72. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_17 line 474
73. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_18 line 481
74. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_18 line 483
75. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_18 line 487
76. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_18 line 500
77. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_19 line 507
78. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_19 line 509
79. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_19 line 513
80. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_19 line 526
81. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_20 line 533
82. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_20 line 535
83. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_20 line 539
84. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_20 line 552
85. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_21 line 559
86. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_21 line 561
87. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_21 line 565
88. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_21 line 578
89. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_22 line 585
90. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_22 line 587
91. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_22 line 591
92. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_22 line 604
93. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_23 line 611
94. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_23 line 613
95. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_23 line 617
96. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_23 line 630
97. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_24 line 637
98. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_24 line 639
99. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_24 line 643
100. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_24 line 656
101. def OAI.MUB6.Certificate.GramEntries.Block3.rows25_25 line 663
102. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck25_25 line 665
103. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound25_25 line 669
104. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval25_25 line 682