OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row18.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_0 line 20
2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_0 line 22
3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_0 line 26
4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_0 line 61
5. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_1 line 68
6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_1 line 70
7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_1 line 74
8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_1 line 109
9. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_2 line 116
10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_2 line 118
11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_2 line 122
12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_2 line 157
13. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_3 line 164
14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_3 line 166
15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_3 line 170
16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_3 line 205
17. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_4 line 212
18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_4 line 214
19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_4 line 218
20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_4 line 253
21. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_5 line 260
22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_5 line 262
23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_5 line 266
24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_5 line 301
25. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_6 line 308
26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_6 line 310
27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_6 line 314
28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_6 line 349
29. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_7 line 356
30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_7 line 358
31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_7 line 362
32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_7 line 397
33. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_8 line 404
34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_8 line 406
35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_8 line 410
36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_8 line 445
37. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_9 line 452
38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_9 line 454
39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_9 line 458
40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_9 line 493
41. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_10 line 500
42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_10 line 502
43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_10 line 506
44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_10 line 541
45. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_11 line 548
46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_11 line 550
47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_11 line 554
48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_11 line 589
49. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_12 line 596
50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_12 line 598
51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_12 line 602
52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_12 line 637
53. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_13 line 644
54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_13 line 646
55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_13 line 650
56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_13 line 685
57. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_14 line 692
58. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_14 line 694
59. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_14 line 698
60. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_14 line 733
61. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_15 line 740
62. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_15 line 742
63. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_15 line 746
64. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_15 line 781
65. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_16 line 788
66. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_16 line 790
67. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_16 line 794
68. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_16 line 829
69. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_17 line 836
70. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_17 line 838
71. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_17 line 842
72. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_17 line 877
73. def OAI.MUB6.Certificate.GramEntries.Block1.rows18_18 line 884
74. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck18_18 line 886
75. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound18_18 line 890
76. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval18_18 line 925