OAI/Analysis/MutuallyUnbiased/GramEntries/Block4Row19.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_0 line 13
2. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_0 line 15
3. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_0 line 19
4. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_0 line 34
5. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_1 line 41
6. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_1 line 43
7. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_1 line 47
8. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_1 line 62
9. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_2 line 69
10. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_2 line 71
11. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_2 line 75
12. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_2 line 90
13. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_3 line 97
14. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_3 line 99
15. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_3 line 103
16. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_3 line 118
17. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_4 line 125
18. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_4 line 127
19. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_4 line 131
20. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_4 line 146
21. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_5 line 153
22. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_5 line 155
23. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_5 line 159
24. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_5 line 174
25. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_6 line 181
26. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_6 line 183
27. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_6 line 187
28. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_6 line 202
29. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_7 line 209
30. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_7 line 211
31. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_7 line 215
32. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_7 line 230
33. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_8 line 237
34. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_8 line 239
35. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_8 line 243
36. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_8 line 258
37. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_9 line 265
38. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_9 line 267
39. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_9 line 271
40. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_9 line 286
41. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_10 line 293
42. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_10 line 295
43. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_10 line 299
44. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_10 line 314
45. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_11 line 321
46. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_11 line 323
47. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_11 line 327
48. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_11 line 342
49. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_12 line 349
50. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_12 line 351
51. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_12 line 355
52. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_12 line 370
53. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_13 line 377
54. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_13 line 379
55. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_13 line 383
56. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_13 line 398
57. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_14 line 405
58. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_14 line 407
59. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_14 line 411
60. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_14 line 426
61. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_15 line 433
62. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_15 line 435
63. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_15 line 439
64. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_15 line 454
65. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_16 line 461
66. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_16 line 463
67. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_16 line 467
68. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_16 line 482
69. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_17 line 489
70. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_17 line 491
71. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_17 line 495
72. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_17 line 510
73. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_18 line 517
74. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_18 line 519
75. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_18 line 523
76. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_18 line 538
77. def OAI.MUB6.Certificate.GramEntries.Block4.rows19_19 line 545
78. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryCheck19_19 line 547
79. theorem OAI.MUB6.Certificate.GramEntries.Block4.rowsSound19_19 line 551
80. theorem OAI.MUB6.Certificate.GramEntries.Block4.entryEval19_19 line 566