OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row26.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_0 line 18
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_0 line 20
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_0 line 24
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_0 line 53
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_1 line 60
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_1 line 62
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_1 line 66
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_1 line 95
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_2 line 102
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_2 line 104
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_2 line 108
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_2 line 137
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_3 line 144
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_3 line 146
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_3 line 150
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_3 line 179
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_4 line 186
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_4 line 188
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_4 line 192
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_4 line 221
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_5 line 228
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_5 line 230
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_5 line 234
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_5 line 263
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_6 line 270
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_6 line 272
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_6 line 276
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_6 line 305
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_7 line 312
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_7 line 314
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_7 line 318
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_7 line 347
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_8 line 354
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_8 line 356
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_8 line 360
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_8 line 389
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_9 line 396
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_9 line 398
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_9 line 402
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_9 line 431
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_10 line 438
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_10 line 440
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_10 line 444
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_10 line 473
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_11 line 480
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_11 line 482
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_11 line 486
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_11 line 515
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_12 line 522
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_12 line 524
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_12 line 528
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_12 line 557
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_13 line 564
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_13 line 566
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_13 line 570
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_13 line 599
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_14 line 606
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_14 line 608
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_14 line 612
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_14 line 641
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_15 line 648
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_15 line 650
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_15 line 654
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_15 line 683
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_16 line 690
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_16 line 692
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_16 line 696
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_16 line 725
69. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_17 line 732
70. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_17 line 734
71. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_17 line 738
72. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_17 line 767
73. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_18 line 774
74. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_18 line 776
75. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_18 line 780
76. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_18 line 809
77. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_19 line 816
78. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_19 line 818
79. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_19 line 822
80. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_19 line 851
81. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_20 line 858
82. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_20 line 860
83. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_20 line 864
84. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_20 line 893
85. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_21 line 900
86. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_21 line 902
87. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_21 line 906
88. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_21 line 935
89. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_22 line 942
90. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_22 line 944
91. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_22 line 948
92. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_22 line 977
93. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_23 line 984
94. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_23 line 986
95. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_23 line 990
96. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_23 line 1019
97. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_24 line 1026
98. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_24 line 1028
99. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_24 line 1032
100. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_24 line 1061
101. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_25 line 1068
102. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_25 line 1070
103. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_25 line 1074
104. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_25 line 1103
105. def OAI.MUB6.Certificate.GramEntries.Block3.rows26_26 line 1110
106. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck26_26 line 1112
107. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound26_26 line 1116
108. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval26_26 line 1145