OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part16.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block3.node512 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node512_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node512_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block3.node513 line 18
5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node513_check line 20
6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node513_eval line 23
7. def OAI.MUB6.Certificate.GramAssembly.Block3.node514 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node514_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node514_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block3.node515 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node515_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node515_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block3.node516 line 49
14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node516_check line 51
15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node516_eval line 54
16. def OAI.MUB6.Certificate.GramAssembly.Block3.node517 line 59
17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node517_check line 61
18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node517_eval line 64
19. def OAI.MUB6.Certificate.GramAssembly.Block3.node518 line 69
20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node518_check line 71
21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node518_eval line 74
22. def OAI.MUB6.Certificate.GramAssembly.Block3.node519 line 79
23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node519_check line 81
24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node519_eval line 84
25. def OAI.MUB6.Certificate.GramAssembly.Block3.node520 line 89
26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node520_check line 91
27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node520_eval line 94
28. def OAI.MUB6.Certificate.GramAssembly.Block3.node521 line 99
29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node521_check line 101
30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node521_eval line 104
31. def OAI.MUB6.Certificate.GramAssembly.Block3.node522 line 110
32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node522_check line 112
33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node522_eval line 115
34. def OAI.MUB6.Certificate.GramAssembly.Block3.node523 line 120
35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node523_check line 122
36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node523_eval line 125
37. def OAI.MUB6.Certificate.GramAssembly.Block3.node524 line 131
38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node524_check line 133
39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node524_eval line 136
40. def OAI.MUB6.Certificate.GramAssembly.Block3.node525 line 141
41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node525_check line 143
42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node525_eval line 146
43. def OAI.MUB6.Certificate.GramAssembly.Block3.node526 line 151
44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node526_check line 153
45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node526_eval line 156
46. def OAI.MUB6.Certificate.GramAssembly.Block3.node527 line 162
47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node527_check line 164
48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node527_eval line 167
49. def OAI.MUB6.Certificate.GramAssembly.Block3.node528 line 172
50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node528_check line 174
51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node528_eval line 177
52. def OAI.MUB6.Certificate.GramAssembly.Block3.node529 line 182
53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node529_check line 184
54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node529_eval line 187
55. def OAI.MUB6.Certificate.GramAssembly.Block3.node530 line 192
56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node530_check line 194
57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node530_eval line 197
58. def OAI.MUB6.Certificate.GramAssembly.Block3.node531 line 202
59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node531_check line 204
60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node531_eval line 207
61. def OAI.MUB6.Certificate.GramAssembly.Block3.node532 line 212
62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node532_check line 214
63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node532_eval line 217
64. def OAI.MUB6.Certificate.GramAssembly.Block3.node533 line 222
65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node533_check line 224
66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node533_eval line 227
67. def OAI.MUB6.Certificate.GramAssembly.Block3.node534 line 233
68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node534_check line 235
69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node534_eval line 238
70. def OAI.MUB6.Certificate.GramAssembly.Block3.node535 line 243
71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node535_check line 245
72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node535_eval line 248
73. def OAI.MUB6.Certificate.GramAssembly.Block3.node536 line 253
74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node536_check line 255
75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node536_eval line 258
76. def OAI.MUB6.Certificate.GramAssembly.Block3.node537 line 263
77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node537_check line 265
78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node537_eval line 268
79. def OAI.MUB6.Certificate.GramAssembly.Block3.node538 line 273
80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node538_check line 275
81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node538_eval line 278
82. def OAI.MUB6.Certificate.GramAssembly.Block3.node539 line 283
83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node539_check line 285
84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node539_eval line 288
85. def OAI.MUB6.Certificate.GramAssembly.Block3.node540 line 294
86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node540_check line 296
87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node540_eval line 299
88. def OAI.MUB6.Certificate.GramAssembly.Block3.node541 line 304
89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node541_check line 306
90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node541_eval line 309
91. def OAI.MUB6.Certificate.GramAssembly.Block3.node542 line 314
92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node542_check line 316
93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node542_eval line 319
94. def OAI.MUB6.Certificate.GramAssembly.Block3.node543 line 324
95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node543_check line 326
96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node543_eval line 329