OAI/Analysis/MutuallyUnbiased/GramEntries/Block1Row19.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_0 line 14
2. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_0 line 16
3. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_0 line 20
4. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_0 line 39
5. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_1 line 46
6. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_1 line 48
7. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_1 line 52
8. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_1 line 71
9. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_2 line 78
10. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_2 line 80
11. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_2 line 84
12. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_2 line 103
13. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_3 line 110
14. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_3 line 112
15. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_3 line 116
16. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_3 line 135
17. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_4 line 142
18. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_4 line 144
19. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_4 line 148
20. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_4 line 167
21. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_5 line 174
22. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_5 line 176
23. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_5 line 180
24. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_5 line 199
25. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_6 line 206
26. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_6 line 208
27. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_6 line 212
28. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_6 line 231
29. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_7 line 238
30. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_7 line 240
31. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_7 line 244
32. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_7 line 263
33. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_8 line 270
34. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_8 line 272
35. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_8 line 276
36. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_8 line 295
37. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_9 line 302
38. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_9 line 304
39. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_9 line 308
40. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_9 line 327
41. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_10 line 334
42. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_10 line 336
43. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_10 line 340
44. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_10 line 359
45. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_11 line 366
46. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_11 line 368
47. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_11 line 372
48. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_11 line 391
49. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_12 line 398
50. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_12 line 400
51. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_12 line 404
52. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_12 line 423
53. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_13 line 430
54. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_13 line 432
55. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_13 line 436
56. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_13 line 455
57. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_14 line 462
58. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_14 line 464
59. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_14 line 468
60. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_14 line 487
61. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_15 line 494
62. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_15 line 496
63. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_15 line 500
64. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_15 line 519
65. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_16 line 526
66. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_16 line 528
67. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_16 line 532
68. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_16 line 551
69. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_17 line 558
70. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_17 line 560
71. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_17 line 564
72. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_17 line 583
73. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_18 line 590
74. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_18 line 592
75. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_18 line 596
76. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_18 line 615
77. def OAI.MUB6.Certificate.GramEntries.Block1.rows19_19 line 622
78. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryCheck19_19 line 624
79. theorem OAI.MUB6.Certificate.GramEntries.Block1.rowsSound19_19 line 628
80. theorem OAI.MUB6.Certificate.GramEntries.Block1.entryEval19_19 line 647