OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row15.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_0 line 16
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_0 line 18
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_0 line 22
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_0 line 43
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_1 line 50
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_1 line 52
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_1 line 56
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_1 line 77
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_2 line 84
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_2 line 86
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_2 line 90
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_2 line 111
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_3 line 118
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_3 line 120
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_3 line 124
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_3 line 145
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_4 line 152
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_4 line 154
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_4 line 158
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_4 line 179
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_5 line 186
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_5 line 188
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_5 line 192
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_5 line 213
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_6 line 220
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_6 line 222
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_6 line 226
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_6 line 247
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_7 line 254
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_7 line 256
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_7 line 260
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_7 line 281
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_8 line 288
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_8 line 290
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_8 line 294
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_8 line 315
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_9 line 322
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_9 line 324
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_9 line 328
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_9 line 349
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_10 line 356
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_10 line 358
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_10 line 362
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_10 line 383
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_11 line 390
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_11 line 392
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_11 line 396
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_11 line 417
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_12 line 424
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_12 line 426
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_12 line 430
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_12 line 451
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_13 line 458
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_13 line 460
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_13 line 464
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_13 line 485
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_14 line 492
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_14 line 494
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_14 line 498
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_14 line 519
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows15_15 line 526
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck15_15 line 528
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound15_15 line 532
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval15_15 line 553