OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part15.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node480 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node480_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node480_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node481 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node481_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node481_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node482 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node482_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node482_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node483 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node483_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node483_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node484 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node484_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node484_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node485 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node485_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node485_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node486 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node486_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node486_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node487 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node487_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node487_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node488 line 90
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node488_check line 92
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node488_eval line 95
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node489 line 100
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node489_check line 102
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node489_eval line 105
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node490 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node490_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node490_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node491 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node491_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node491_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node492 line 130
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node492_check line 132
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node492_eval line 135
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node493 line 140
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node493_check line 142
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node493_eval line 145
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node494 line 150
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node494_check line 152
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node494_eval line 155
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node495 line 160
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node495_check line 162
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node495_eval line 165
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node496 line 171
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node496_check line 173
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node496_eval line 176
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node497 line 181
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node497_check line 183
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node497_eval line 186
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node498 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node498_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node498_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node499 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node499_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node499_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node500 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node500_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node500_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node501 line 223
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node501_check line 225
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node501_eval line 228
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node502 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node502_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node502_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node503 line 243
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node503_check line 245
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node503_eval line 248
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node504 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node504_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node504_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node505 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node505_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node505_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node506 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node506_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node506_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node507 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node507_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node507_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node508 line 294
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node508_check line 296
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node508_eval line 299
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node509 line 304
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node509_check line 306
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node509_eval line 309
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node510 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node510_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node510_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node511 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node511_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node511_eval line 329