OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row16.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_0 line 17
2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_0 line 19
3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_0 line 23
4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_0 line 64
5. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_1 line 71
6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_1 line 73
7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_1 line 77
8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_1 line 118
9. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_2 line 125
10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_2 line 127
11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_2 line 131
12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_2 line 172
13. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_3 line 179
14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_3 line 181
15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_3 line 185
16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_3 line 226
17. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_4 line 233
18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_4 line 235
19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_4 line 239
20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_4 line 280
21. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_5 line 287
22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_5 line 289
23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_5 line 293
24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_5 line 334
25. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_6 line 341
26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_6 line 343
27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_6 line 347
28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_6 line 388
29. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_7 line 395
30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_7 line 397
31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_7 line 401
32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_7 line 442
33. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_8 line 449
34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_8 line 451
35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_8 line 455
36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_8 line 496
37. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_9 line 503
38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_9 line 505
39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_9 line 509
40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_9 line 550
41. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_10 line 557
42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_10 line 559
43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_10 line 563
44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_10 line 604
45. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_11 line 611
46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_11 line 613
47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_11 line 617
48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_11 line 658
49. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_12 line 665
50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_12 line 667
51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_12 line 671
52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_12 line 712
53. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_13 line 719
54. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_13 line 721
55. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_13 line 725
56. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_13 line 766
57. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_14 line 773
58. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_14 line 775
59. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_14 line 779
60. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_14 line 820
61. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_15 line 827
62. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_15 line 829
63. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_15 line 833
64. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_15 line 874
65. def OAI.MUB6.Certificate.GramEntries.Block4.rows16_16 line 881
66. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck16_16 line 883
67. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound16_16 line 887
68. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval16_16 line 928