OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row16.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_0 line 17
2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_0 line 19
3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_0 line 23
4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_0 line 46
5. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_1 line 53
6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_1 line 55
7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_1 line 59
8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_1 line 82
9. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_2 line 89
10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_2 line 91
11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_2 line 95
12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_2 line 118
13. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_3 line 125
14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_3 line 127
15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_3 line 131
16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_3 line 154
17. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_4 line 161
18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_4 line 163
19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_4 line 167
20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_4 line 190
21. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_5 line 197
22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_5 line 199
23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_5 line 203
24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_5 line 226
25. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_6 line 233
26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_6 line 235
27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_6 line 239
28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_6 line 262
29. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_7 line 269
30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_7 line 271
31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_7 line 275
32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_7 line 298
33. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_8 line 305
34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_8 line 307
35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_8 line 311
36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_8 line 334
37. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_9 line 341
38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_9 line 343
39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_9 line 347
40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_9 line 370
41. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_10 line 377
42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_10 line 379
43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_10 line 383
44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_10 line 406
45. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_11 line 413
46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_11 line 415
47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_11 line 419
48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_11 line 442
49. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_12 line 449
50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_12 line 451
51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_12 line 455
52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_12 line 478
53. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_13 line 485
54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_13 line 487
55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_13 line 491
56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_13 line 514
57. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_14 line 521
58. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_14 line 523
59. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_14 line 527
60. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_14 line 550
61. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_15 line 557
62. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_15 line 559
63. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_15 line 563
64. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_15 line 586
65. def OAI.MUB6.Certificate.GramEntries.Block1.rows16_16 line 593
66. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck16_16 line 595
67. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound16_16 line 599
68. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval16_16 line 622