OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row23.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_0 line 16
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_0 line 18
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_0 line 22
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_0 line 45
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_1 line 52
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_1 line 54
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_1 line 58
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_1 line 81
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_2 line 88
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_2 line 90
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_2 line 94
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_2 line 117
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_3 line 124
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_3 line 126
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_3 line 130
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_3 line 153
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_4 line 160
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_4 line 162
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_4 line 166
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_4 line 189
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_5 line 196
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_5 line 198
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_5 line 202
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_5 line 225
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_6 line 232
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_6 line 234
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_6 line 238
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_6 line 261
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_7 line 268
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_7 line 270
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_7 line 274
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_7 line 297
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_8 line 304
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_8 line 306
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_8 line 310
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_8 line 333
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_9 line 340
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_9 line 342
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_9 line 346
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_9 line 369
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_10 line 376
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_10 line 378
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_10 line 382
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_10 line 405
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_11 line 412
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_11 line 414
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_11 line 418
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_11 line 441
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_12 line 448
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_12 line 450
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_12 line 454
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_12 line 477
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_13 line 484
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_13 line 486
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_13 line 490
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_13 line 513
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_14 line 520
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_14 line 522
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_14 line 526
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_14 line 549
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_15 line 556
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_15 line 558
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_15 line 562
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_15 line 585
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_16 line 592
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_16 line 594
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_16 line 598
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_16 line 621
69. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_17 line 628
70. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_17 line 630
71. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_17 line 634
72. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_17 line 657
73. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_18 line 664
74. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_18 line 666
75. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_18 line 670
76. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_18 line 693
77. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_19 line 700
78. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_19 line 702
79. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_19 line 706
80. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_19 line 729
81. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_20 line 736
82. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_20 line 738
83. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_20 line 742
84. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_20 line 765
85. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_21 line 772
86. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_21 line 774
87. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_21 line 778
88. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_21 line 801
89. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_22 line 808
90. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_22 line 810
91. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_22 line 814
92. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_22 line 837
93. def OAI.MUB6.Certificate.GramEntries.Block3.rows23_23 line 844
94. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck23_23 line 846
95. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound23_23 line 850
96. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval23_23 line 873