OAI/Analysis/MutuallyUnbiased/GramEntries/Block3Row20.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_0 line 13
2. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_0 line 15
3. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_0 line 19
4. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_0 line 29
5. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_1 line 36
6. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_1 line 38
7. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_1 line 42
8. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_1 line 52
9. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_2 line 59
10. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_2 line 61
11. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_2 line 65
12. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_2 line 75
13. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_3 line 82
14. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_3 line 84
15. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_3 line 88
16. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_3 line 98
17. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_4 line 105
18. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_4 line 107
19. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_4 line 111
20. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_4 line 121
21. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_5 line 128
22. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_5 line 130
23. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_5 line 134
24. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_5 line 144
25. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_6 line 151
26. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_6 line 153
27. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_6 line 157
28. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_6 line 167
29. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_7 line 174
30. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_7 line 176
31. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_7 line 180
32. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_7 line 190
33. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_8 line 197
34. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_8 line 199
35. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_8 line 203
36. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_8 line 213
37. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_9 line 220
38. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_9 line 222
39. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_9 line 226
40. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_9 line 236
41. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_10 line 243
42. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_10 line 245
43. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_10 line 249
44. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_10 line 259
45. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_11 line 266
46. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_11 line 268
47. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_11 line 272
48. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_11 line 282
49. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_12 line 289
50. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_12 line 291
51. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_12 line 295
52. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_12 line 305
53. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_13 line 312
54. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_13 line 314
55. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_13 line 318
56. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_13 line 328
57. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_14 line 335
58. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_14 line 337
59. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_14 line 341
60. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_14 line 351
61. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_15 line 358
62. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_15 line 360
63. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_15 line 364
64. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_15 line 374
65. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_16 line 381
66. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_16 line 383
67. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_16 line 387
68. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_16 line 397
69. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_17 line 404
70. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_17 line 406
71. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_17 line 410
72. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_17 line 420
73. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_18 line 427
74. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_18 line 429
75. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_18 line 433
76. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_18 line 443
77. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_19 line 450
78. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_19 line 452
79. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_19 line 456
80. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_19 line 466
81. def OAI.MUB6.Certificate.GramEntries.Block3.rows20_20 line 473
82. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryCheck20_20 line 475
83. theorem OAI.MUB6.Certificate.GramEntries.Block3.rowsSound20_20 line 479
84. theorem OAI.MUB6.Certificate.GramEntries.Block3.entryEval20_20 line 489