OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row15.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_0 line 20
2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_0 line 22
3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_0 line 26
4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_0 line 61
5. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_1 line 68
6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_1 line 70
7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_1 line 74
8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_1 line 109
9. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_2 line 116
10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_2 line 118
11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_2 line 122
12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_2 line 157
13. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_3 line 164
14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_3 line 166
15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_3 line 170
16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_3 line 205
17. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_4 line 212
18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_4 line 214
19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_4 line 218
20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_4 line 253
21. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_5 line 260
22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_5 line 262
23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_5 line 266
24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_5 line 301
25. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_6 line 308
26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_6 line 310
27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_6 line 314
28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_6 line 349
29. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_7 line 356
30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_7 line 358
31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_7 line 362
32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_7 line 397
33. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_8 line 404
34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_8 line 406
35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_8 line 410
36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_8 line 445
37. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_9 line 452
38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_9 line 454
39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_9 line 458
40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_9 line 493
41. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_10 line 500
42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_10 line 502
43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_10 line 506
44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_10 line 541
45. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_11 line 548
46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_11 line 550
47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_11 line 554
48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_11 line 589
49. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_12 line 596
50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_12 line 598
51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_12 line 602
52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_12 line 637
53. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_13 line 644
54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_13 line 646
55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_13 line 650
56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_13 line 685
57. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_14 line 692
58. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_14 line 694
59. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_14 line 698
60. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_14 line 733
61. def OAI.MUB6.Certificate.GramEntries.Block1.rows15_15 line 740
62. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck15_15 line 742
63. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound15_15 line 746
64. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval15_15 line 781