OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part3.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.GramAssembly.Block4.node96 line 8
2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node96_check line 10
3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node96_eval line 13
4. def OAI.MUB6.Certificate.GramAssembly.Block4.node97 line 19
5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node97_check line 21
6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node97_eval line 24
7. def OAI.MUB6.Certificate.GramAssembly.Block4.node98 line 29
8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node98_check line 31
9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node98_eval line 34
10. def OAI.MUB6.Certificate.GramAssembly.Block4.node99 line 39
11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node99_check line 41
12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node99_eval line 44
13. def OAI.MUB6.Certificate.GramAssembly.Block4.node100 line 50
14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node100_check line 52
15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node100_eval line 55
16. def OAI.MUB6.Certificate.GramAssembly.Block4.node101 line 60
17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node101_check line 62
18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node101_eval line 65
19. def OAI.MUB6.Certificate.GramAssembly.Block4.node102 line 71
20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node102_check line 73
21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node102_eval line 76
22. def OAI.MUB6.Certificate.GramAssembly.Block4.node103 line 81
23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node103_check line 83
24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node103_eval line 86
25. def OAI.MUB6.Certificate.GramAssembly.Block4.node104 line 91
26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node104_check line 93
27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node104_eval line 96
28. def OAI.MUB6.Certificate.GramAssembly.Block4.node105 line 101
29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node105_check line 103
30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node105_eval line 106
31. def OAI.MUB6.Certificate.GramAssembly.Block4.node106 line 111
32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node106_check line 113
33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node106_eval line 116
34. def OAI.MUB6.Certificate.GramAssembly.Block4.node107 line 121
35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node107_check line 123
36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node107_eval line 126
37. def OAI.MUB6.Certificate.GramAssembly.Block4.node108 line 132
38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node108_check line 134
39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node108_eval line 137
40. def OAI.MUB6.Certificate.GramAssembly.Block4.node109 line 142
41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node109_check line 144
42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node109_eval line 147
43. def OAI.MUB6.Certificate.GramAssembly.Block4.node110 line 152
44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node110_check line 154
45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node110_eval line 157
46. def OAI.MUB6.Certificate.GramAssembly.Block4.node111 line 163
47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node111_check line 165
48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node111_eval line 168
49. def OAI.MUB6.Certificate.GramAssembly.Block4.node112 line 173
50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node112_check line 175
51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node112_eval line 178
52. def OAI.MUB6.Certificate.GramAssembly.Block4.node113 line 184
53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node113_check line 186
54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node113_eval line 189
55. def OAI.MUB6.Certificate.GramAssembly.Block4.node114 line 194
56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node114_check line 196
57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node114_eval line 199
58. def OAI.MUB6.Certificate.GramAssembly.Block4.node115 line 204
59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node115_check line 206
60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node115_eval line 209
61. def OAI.MUB6.Certificate.GramAssembly.Block4.node116 line 214
62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node116_check line 216
63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node116_eval line 219
64. def OAI.MUB6.Certificate.GramAssembly.Block4.node117 line 224
65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node117_check line 226
66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node117_eval line 229
67. def OAI.MUB6.Certificate.GramAssembly.Block4.node118 line 235
68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node118_check line 237
69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node118_eval line 240
70. def OAI.MUB6.Certificate.GramAssembly.Block4.node119 line 245
71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node119_check line 247
72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node119_eval line 250
73. def OAI.MUB6.Certificate.GramAssembly.Block4.node120 line 255
74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node120_check line 257
75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node120_eval line 260
76. def OAI.MUB6.Certificate.GramAssembly.Block4.node121 line 266
77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node121_check line 268
78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node121_eval line 271
79. def OAI.MUB6.Certificate.GramAssembly.Block4.node122 line 276
80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node122_check line 278
81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node122_eval line 281
82. def OAI.MUB6.Certificate.GramAssembly.Block4.node123 line 287
83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node123_check line 289
84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node123_eval line 292
85. def OAI.MUB6.Certificate.GramAssembly.Block4.node124 line 297
86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node124_check line 299
87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node124_eval line 302
88. def OAI.MUB6.Certificate.GramAssembly.Block4.node125 line 307
89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node125_check line 309
90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node125_eval line 312
91. def OAI.MUB6.Certificate.GramAssembly.Block4.node126 line 317
92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node126_check line 319
93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node126_eval line 322
94. def OAI.MUB6.Certificate.GramAssembly.Block4.node127 line 327
95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node127_check line 329
96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node127_eval line 332