OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row18.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_0 line 15
2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_0 line 17
3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_0 line 21
4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_0 line 46
5. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_1 line 53
6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_1 line 55
7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_1 line 59
8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_1 line 84
9. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_2 line 91
10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_2 line 93
11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_2 line 97
12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_2 line 122
13. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_3 line 129
14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_3 line 131
15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_3 line 135
16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_3 line 160
17. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_4 line 167
18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_4 line 169
19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_4 line 173
20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_4 line 198
21. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_5 line 205
22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_5 line 207
23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_5 line 211
24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_5 line 236
25. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_6 line 243
26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_6 line 245
27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_6 line 249
28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_6 line 274
29. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_7 line 281
30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_7 line 283
31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_7 line 287
32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_7 line 312
33. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_8 line 319
34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_8 line 321
35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_8 line 325
36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_8 line 350
37. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_9 line 357
38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_9 line 359
39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_9 line 363
40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_9 line 388
41. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_10 line 395
42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_10 line 397
43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_10 line 401
44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_10 line 426
45. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_11 line 433
46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_11 line 435
47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_11 line 439
48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_11 line 464
49. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_12 line 471
50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_12 line 473
51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_12 line 477
52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_12 line 502
53. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_13 line 509
54. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_13 line 511
55. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_13 line 515
56. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_13 line 540
57. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_14 line 547
58. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_14 line 549
59. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_14 line 553
60. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_14 line 578
61. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_15 line 585
62. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_15 line 587
63. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_15 line 591
64. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_15 line 616
65. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_16 line 623
66. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_16 line 625
67. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_16 line 629
68. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_16 line 654
69. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_17 line 661
70. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_17 line 663
71. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_17 line 667
72. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_17 line 692
73. def OAI.MUB6.Certificate.GramEntries.Block4.rows18_18 line 699
74. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck18_18 line 701
75. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound18_18 line 705
76. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval18_18 line 730