OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part11.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block3.node352 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node352_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node352_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block3.node353 line 18
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node353_check line 20
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node353_eval line 23
  7. def OAI.MUB6.Certificate.GramAssembly.Block3.node354 line 28
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node354_check line 30
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node354_eval line 33
  10. def OAI.MUB6.Certificate.GramAssembly.Block3.node355 line 38
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node355_check line 40
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node355_eval line 43
  13. def OAI.MUB6.Certificate.GramAssembly.Block3.node356 line 48
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node356_check line 50
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node356_eval line 53
  16. def OAI.MUB6.Certificate.GramAssembly.Block3.node357 line 58
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node357_check line 60
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node357_eval line 63
  19. def OAI.MUB6.Certificate.GramAssembly.Block3.node358 line 69
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node358_check line 71
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node358_eval line 74
  22. def OAI.MUB6.Certificate.GramAssembly.Block3.node359 line 79
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node359_check line 81
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node359_eval line 84
  25. def OAI.MUB6.Certificate.GramAssembly.Block3.node360 line 89
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node360_check line 91
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node360_eval line 94
  28. def OAI.MUB6.Certificate.GramAssembly.Block3.node361 line 99
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node361_check line 101
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node361_eval line 104
  31. def OAI.MUB6.Certificate.GramAssembly.Block3.node362 line 109
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node362_check line 111
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node362_eval line 114
  34. def OAI.MUB6.Certificate.GramAssembly.Block3.node363 line 119
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node363_check line 121
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node363_eval line 124
  37. def OAI.MUB6.Certificate.GramAssembly.Block3.node364 line 129
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node364_check line 131
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node364_eval line 134
  40. def OAI.MUB6.Certificate.GramAssembly.Block3.node365 line 139
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node365_check line 141
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node365_eval line 144
  43. def OAI.MUB6.Certificate.GramAssembly.Block3.node366 line 150
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node366_check line 152
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node366_eval line 155
  46. def OAI.MUB6.Certificate.GramAssembly.Block3.node367 line 160
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node367_check line 162
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node367_eval line 165
  49. def OAI.MUB6.Certificate.GramAssembly.Block3.node368 line 171
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node368_check line 173
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node368_eval line 176
  52. def OAI.MUB6.Certificate.GramAssembly.Block3.node369 line 181
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node369_check line 183
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node369_eval line 186
  55. def OAI.MUB6.Certificate.GramAssembly.Block3.node370 line 191
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node370_check line 193
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node370_eval line 196
  58. def OAI.MUB6.Certificate.GramAssembly.Block3.node371 line 202
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node371_check line 204
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node371_eval line 207
  61. def OAI.MUB6.Certificate.GramAssembly.Block3.node372 line 212
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node372_check line 214
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node372_eval line 217
  64. def OAI.MUB6.Certificate.GramAssembly.Block3.node373 line 222
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node373_check line 224
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node373_eval line 227
  67. def OAI.MUB6.Certificate.GramAssembly.Block3.node374 line 232
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node374_check line 234
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node374_eval line 237
  70. def OAI.MUB6.Certificate.GramAssembly.Block3.node375 line 242
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node375_check line 244
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node375_eval line 247
  73. def OAI.MUB6.Certificate.GramAssembly.Block3.node376 line 252
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node376_check line 254
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node376_eval line 257
  76. def OAI.MUB6.Certificate.GramAssembly.Block3.node377 line 262
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node377_check line 264
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node377_eval line 267
  79. def OAI.MUB6.Certificate.GramAssembly.Block3.node378 line 273
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node378_check line 275
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node378_eval line 278
  82. def OAI.MUB6.Certificate.GramAssembly.Block3.node379 line 283
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node379_check line 285
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node379_eval line 288
  85. def OAI.MUB6.Certificate.GramAssembly.Block3.node380 line 293
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node380_check line 295
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node380_eval line 298
  88. def OAI.MUB6.Certificate.GramAssembly.Block3.node381 line 303
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node381_check line 305
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node381_eval line 308
  91. def OAI.MUB6.Certificate.GramAssembly.Block3.node382 line 313
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node382_check line 315
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node382_eval line 318
  94. def OAI.MUB6.Certificate.GramAssembly.Block3.node383 line 323
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node383_check line 325
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node383_eval line 328