OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part17.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block3.node544 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node544_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node544_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block3.node545 line 18
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node545_check line 20
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node545_eval line 23
  7. def OAI.MUB6.Certificate.GramAssembly.Block3.node546 line 28
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node546_check line 30
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node546_eval line 33
  10. def OAI.MUB6.Certificate.GramAssembly.Block3.node547 line 38
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node547_check line 40
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node547_eval line 43
  13. def OAI.MUB6.Certificate.GramAssembly.Block3.node548 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node548_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node548_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block3.node549 line 59
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node549_check line 61
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node549_eval line 64
  19. def OAI.MUB6.Certificate.GramAssembly.Block3.node550 line 70
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node550_check line 72
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node550_eval line 75
  22. def OAI.MUB6.Certificate.GramAssembly.Block3.node551 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node551_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node551_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block3.node552 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node552_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node552_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block3.node553 line 101
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node553_check line 103
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node553_eval line 106
  31. def OAI.MUB6.Certificate.GramAssembly.Block3.node554 line 111
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node554_check line 113
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node554_eval line 116
  34. def OAI.MUB6.Certificate.GramAssembly.Block3.node555 line 121
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node555_check line 123
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node555_eval line 126
  37. def OAI.MUB6.Certificate.GramAssembly.Block3.node556 line 131
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node556_check line 133
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node556_eval line 136
  40. def OAI.MUB6.Certificate.GramAssembly.Block3.node557 line 141
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node557_check line 143
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node557_eval line 146
  43. def OAI.MUB6.Certificate.GramAssembly.Block3.node558 line 151
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node558_check line 153
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node558_eval line 156
  46. def OAI.MUB6.Certificate.GramAssembly.Block3.node559 line 161
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node559_check line 163
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node559_eval line 166
  49. def OAI.MUB6.Certificate.GramAssembly.Block3.node560 line 172
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node560_check line 174
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node560_eval line 177
  52. def OAI.MUB6.Certificate.GramAssembly.Block3.node561 line 182
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node561_check line 184
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node561_eval line 187
  55. def OAI.MUB6.Certificate.GramAssembly.Block3.node562 line 192
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node562_check line 194
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node562_eval line 197
  58. def OAI.MUB6.Certificate.GramAssembly.Block3.node563 line 202
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node563_check line 204
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node563_eval line 207
  61. def OAI.MUB6.Certificate.GramAssembly.Block3.node564 line 212
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node564_check line 214
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node564_eval line 217
  64. def OAI.MUB6.Certificate.GramAssembly.Block3.node565 line 222
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node565_check line 224
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node565_eval line 227
  67. def OAI.MUB6.Certificate.GramAssembly.Block3.node566 line 233
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node566_check line 235
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node566_eval line 238
  70. def OAI.MUB6.Certificate.GramAssembly.Block3.node567 line 243
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node567_check line 245
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node567_eval line 248
  73. def OAI.MUB6.Certificate.GramAssembly.Block3.node568 line 253
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node568_check line 255
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node568_eval line 258
  76. def OAI.MUB6.Certificate.GramAssembly.Block3.node569 line 263
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node569_check line 265
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node569_eval line 268
  79. def OAI.MUB6.Certificate.GramAssembly.Block3.node570 line 273
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node570_check line 275
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node570_eval line 278
  82. def OAI.MUB6.Certificate.GramAssembly.Block3.node571 line 283
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node571_check line 285
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node571_eval line 288
  85. def OAI.MUB6.Certificate.GramAssembly.Block3.node572 line 293
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node572_check line 295
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node572_eval line 298
  88. def OAI.MUB6.Certificate.GramAssembly.Block3.node573 line 303
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node573_check line 305
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node573_eval line 308
  91. def OAI.MUB6.Certificate.GramAssembly.Block3.node574 line 314
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node574_check line 316
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node574_eval line 319
  94. def OAI.MUB6.Certificate.GramAssembly.Block3.node575 line 324
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node575_check line 326
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node575_eval line 329