OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row22.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_0 line 21
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_0 line 23
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_0 line 27
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_0 line 68
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_1 line 75
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_1 line 77
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_1 line 81
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_1 line 122
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_2 line 129
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_2 line 131
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_2 line 135
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_2 line 176
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_3 line 183
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_3 line 185
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_3 line 189
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_3 line 230
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_4 line 237
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_4 line 239
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_4 line 243
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_4 line 284
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_5 line 291
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_5 line 293
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_5 line 297
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_5 line 338
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_6 line 345
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_6 line 347
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_6 line 351
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_6 line 392
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_7 line 399
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_7 line 401
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_7 line 405
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_7 line 446
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_8 line 453
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_8 line 455
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_8 line 459
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_8 line 500
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_9 line 507
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_9 line 509
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_9 line 513
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_9 line 554
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_10 line 561
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_10 line 563
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_10 line 567
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_10 line 608
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_11 line 615
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_11 line 617
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_11 line 621
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_11 line 662
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_12 line 669
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_12 line 671
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_12 line 675
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_12 line 716
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_13 line 723
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_13 line 725
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_13 line 729
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_13 line 770
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_14 line 777
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_14 line 779
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_14 line 783
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_14 line 824
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_15 line 831
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_15 line 833
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_15 line 837
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_15 line 878
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_16 line 885
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_16 line 887
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_16 line 891
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_16 line 932
69. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_17 line 939
70. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_17 line 941
71. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_17 line 945
72. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_17 line 986
73. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_18 line 993
74. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_18 line 995
75. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_18 line 999
76. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_18 line 1040
77. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_19 line 1047
78. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_19 line 1049
79. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_19 line 1053
80. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_19 line 1094
81. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_20 line 1101
82. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_20 line 1103
83. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_20 line 1107
84. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_20 line 1148
85. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_21 line 1155
86. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_21 line 1157
87. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_21 line 1161
88. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_21 line 1202
89. def OAI.MUB6.Certificate.GramEntries.Block3.rows22_22 line 1209
90. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck22_22 line 1211
91. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound22_22 line 1215
92. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval22_22 line 1256