OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row15.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_0 line 20
2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_0 line 22
3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_0 line 26
4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_0 line 67
5. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_1 line 74
6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_1 line 76
7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_1 line 80
8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_1 line 121
9. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_2 line 128
10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_2 line 130
11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_2 line 134
12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_2 line 175
13. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_3 line 182
14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_3 line 184
15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_3 line 188
16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_3 line 229
17. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_4 line 236
18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_4 line 238
19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_4 line 242
20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_4 line 283
21. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_5 line 290
22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_5 line 292
23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_5 line 296
24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_5 line 337
25. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_6 line 344
26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_6 line 346
27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_6 line 350
28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_6 line 391
29. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_7 line 398
30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_7 line 400
31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_7 line 404
32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_7 line 445
33. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_8 line 452
34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_8 line 454
35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_8 line 458
36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_8 line 499
37. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_9 line 506
38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_9 line 508
39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_9 line 512
40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_9 line 553
41. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_10 line 560
42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_10 line 562
43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_10 line 566
44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_10 line 607
45. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_11 line 614
46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_11 line 616
47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_11 line 620
48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_11 line 661
49. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_12 line 668
50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_12 line 670
51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_12 line 674
52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_12 line 715
53. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_13 line 722
54. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_13 line 724
55. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_13 line 728
56. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_13 line 769
57. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_14 line 776
58. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_14 line 778
59. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_14 line 782
60. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_14 line 823
61. def OAI.MUB6.Certificate.GramEntries.Block4.rows15_15 line 830
62. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck15_15 line 832
63. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound15_15 line 836
64. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval15_15 line 877