OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row21.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_0 line 15
2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_0 line 17
3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_0 line 21
4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_0 line 46
5. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_1 line 53
6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_1 line 55
7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_1 line 59
8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_1 line 84
9. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_2 line 91
10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_2 line 93
11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_2 line 97
12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_2 line 122
13. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_3 line 129
14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_3 line 131
15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_3 line 135
16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_3 line 160
17. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_4 line 167
18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_4 line 169
19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_4 line 173
20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_4 line 198
21. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_5 line 205
22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_5 line 207
23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_5 line 211
24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_5 line 236
25. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_6 line 243
26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_6 line 245
27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_6 line 249
28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_6 line 274
29. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_7 line 281
30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_7 line 283
31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_7 line 287
32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_7 line 312
33. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_8 line 319
34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_8 line 321
35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_8 line 325
36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_8 line 350
37. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_9 line 357
38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_9 line 359
39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_9 line 363
40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_9 line 388
41. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_10 line 395
42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_10 line 397
43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_10 line 401
44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_10 line 426
45. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_11 line 433
46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_11 line 435
47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_11 line 439
48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_11 line 464
49. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_12 line 471
50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_12 line 473
51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_12 line 477
52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_12 line 502
53. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_13 line 509
54. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_13 line 511
55. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_13 line 515
56. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_13 line 540
57. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_14 line 547
58. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_14 line 549
59. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_14 line 553
60. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_14 line 578
61. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_15 line 585
62. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_15 line 587
63. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_15 line 591
64. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_15 line 616
65. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_16 line 623
66. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_16 line 625
67. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_16 line 629
68. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_16 line 654
69. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_17 line 661
70. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_17 line 663
71. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_17 line 667
72. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_17 line 692
73. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_18 line 699
74. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_18 line 701
75. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_18 line 705
76. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_18 line 730
77. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_19 line 737
78. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_19 line 739
79. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_19 line 743
80. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_19 line 768
81. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_20 line 775
82. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_20 line 777
83. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_20 line 781
84. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_20 line 806
85. def OAI.MUB6.Certificate.GramEntries.Block4.rows21_21 line 813
86. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck21_21 line 815
87. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound21_21 line 819
88. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval21_21 line 844