OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row16.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_0 line 14
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_0 line 16
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_0 line 20
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_0 line 33
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_1 line 40
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_1 line 42
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_1 line 46
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_1 line 59
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_2 line 66
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_2 line 68
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_2 line 72
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_2 line 85
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_3 line 92
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_3 line 94
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_3 line 98
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_3 line 111
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_4 line 118
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_4 line 120
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_4 line 124
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_4 line 137
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_5 line 144
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_5 line 146
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_5 line 150
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_5 line 163
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_6 line 170
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_6 line 172
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_6 line 176
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_6 line 189
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_7 line 196
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_7 line 198
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_7 line 202
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_7 line 215
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_8 line 222
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_8 line 224
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_8 line 228
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_8 line 241
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_9 line 248
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_9 line 250
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_9 line 254
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_9 line 267
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_10 line 274
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_10 line 276
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_10 line 280
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_10 line 293
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_11 line 300
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_11 line 302
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_11 line 306
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_11 line 319
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_12 line 326
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_12 line 328
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_12 line 332
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_12 line 345
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_13 line 352
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_13 line 354
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_13 line 358
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_13 line 371
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_14 line 378
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_14 line 380
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_14 line 384
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_14 line 397
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_15 line 404
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_15 line 406
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_15 line 410
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_15 line 423
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows16_16 line 430
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck16_16 line 432
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound16_16 line 436
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval16_16 line 449