OAI/Analysis/MutuallyUnbiased/GramAssembly/Block1Part6.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block1.node192 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node192_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node192_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block1.node193 line 18
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node193_check line 20
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node193_eval line 23
  7. def OAI.MUB6.Certificate.GramAssembly.Block1.node194 line 28
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node194_check line 30
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node194_eval line 33
  10. def OAI.MUB6.Certificate.GramAssembly.Block1.node195 line 39
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node195_check line 41
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node195_eval line 44
  13. def OAI.MUB6.Certificate.GramAssembly.Block1.node196 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node196_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node196_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block1.node197 line 60
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node197_check line 62
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node197_eval line 65
  19. def OAI.MUB6.Certificate.GramAssembly.Block1.node198 line 70
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node198_check line 72
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node198_eval line 75
  22. def OAI.MUB6.Certificate.GramAssembly.Block1.node199 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node199_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node199_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block1.node200 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node200_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node200_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block1.node201 line 100
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node201_check line 102
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node201_eval line 105
  31. def OAI.MUB6.Certificate.GramAssembly.Block1.node202 line 110
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node202_check line 112
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node202_eval line 115
  34. def OAI.MUB6.Certificate.GramAssembly.Block1.node203 line 121
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node203_check line 123
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node203_eval line 126
  37. def OAI.MUB6.Certificate.GramAssembly.Block1.node204 line 131
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node204_check line 133
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node204_eval line 136
  40. def OAI.MUB6.Certificate.GramAssembly.Block1.node205 line 141
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node205_check line 143
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node205_eval line 146
  43. def OAI.MUB6.Certificate.GramAssembly.Block1.node206 line 151
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node206_check line 153
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node206_eval line 156
  46. def OAI.MUB6.Certificate.GramAssembly.Block1.node207 line 162
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node207_check line 164
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node207_eval line 167
  49. def OAI.MUB6.Certificate.GramAssembly.Block1.node208 line 172
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node208_check line 174
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node208_eval line 177
  52. def OAI.MUB6.Certificate.GramAssembly.Block1.node209 line 182
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node209_check line 184
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node209_eval line 187
  55. def OAI.MUB6.Certificate.GramAssembly.Block1.node210 line 192
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node210_check line 194
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node210_eval line 197
  58. def OAI.MUB6.Certificate.GramAssembly.Block1.node211 line 202
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node211_check line 204
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node211_eval line 207
  61. def OAI.MUB6.Certificate.GramAssembly.Block1.node212 line 213
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node212_check line 215
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node212_eval line 218
  64. def OAI.MUB6.Certificate.GramAssembly.Block1.node213 line 223
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node213_check line 225
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node213_eval line 228
  67. def OAI.MUB6.Certificate.GramAssembly.Block1.node214 line 233
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node214_check line 235
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node214_eval line 238
  70. def OAI.MUB6.Certificate.GramAssembly.Block1.node215 line 244
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node215_check line 246
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node215_eval line 249
  73. def OAI.MUB6.Certificate.GramAssembly.Block1.node216 line 254
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node216_check line 256
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node216_eval line 259
  76. def OAI.MUB6.Certificate.GramAssembly.Block1.node217 line 265
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node217_check line 267
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node217_eval line 270
  79. def OAI.MUB6.Certificate.GramAssembly.Block1.node218 line 275
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node218_check line 277
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node218_eval line 280
  82. def OAI.MUB6.Certificate.GramAssembly.Block1.node219 line 285
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node219_check line 287
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node219_eval line 290
  85. def OAI.MUB6.Certificate.GramAssembly.Block1.node220 line 295
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node220_check line 297
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node220_eval line 300
  88. def OAI.MUB6.Certificate.GramAssembly.Block1.node221 line 305
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node221_check line 307
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node221_eval line 310
  91. def OAI.MUB6.Certificate.GramAssembly.Block1.node222 line 315
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node222_check line 317
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node222_eval line 320
  94. def OAI.MUB6.Certificate.GramAssembly.Block1.node223 line 326
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node223_check line 328
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block1.node223_eval line 331