OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row17.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_0 line 17
2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_0 line 19
3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_0 line 23
4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_0 line 58
5. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_1 line 65
6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_1 line 67
7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_1 line 71
8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_1 line 106
9. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_2 line 113
10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_2 line 115
11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_2 line 119
12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_2 line 154
13. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_3 line 161
14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_3 line 163
15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_3 line 167
16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_3 line 202
17. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_4 line 209
18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_4 line 211
19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_4 line 215
20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_4 line 250
21. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_5 line 257
22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_5 line 259
23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_5 line 263
24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_5 line 298
25. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_6 line 305
26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_6 line 307
27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_6 line 311
28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_6 line 346
29. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_7 line 353
30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_7 line 355
31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_7 line 359
32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_7 line 394
33. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_8 line 401
34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_8 line 403
35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_8 line 407
36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_8 line 442
37. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_9 line 449
38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_9 line 451
39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_9 line 455
40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_9 line 490
41. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_10 line 497
42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_10 line 499
43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_10 line 503
44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_10 line 538
45. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_11 line 545
46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_11 line 547
47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_11 line 551
48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_11 line 586
49. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_12 line 593
50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_12 line 595
51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_12 line 599
52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_12 line 634
53. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_13 line 641
54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_13 line 643
55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_13 line 647
56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_13 line 682
57. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_14 line 689
58. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_14 line 691
59. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_14 line 695
60. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_14 line 730
61. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_15 line 737
62. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_15 line 739
63. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_15 line 743
64. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_15 line 778
65. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_16 line 785
66. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_16 line 787
67. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_16 line 791
68. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_16 line 826
69. def OAI.MUB6.Certificate.GramEntries.Block1.rows17_17 line 833
70. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck17_17 line 835
71. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound17_17 line 839
72. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval17_17 line 874