OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part12.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block4.node384 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node384_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node384_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block4.node385 line 18
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node385_check line 20
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node385_eval line 23
  7. def OAI.MUB6.Certificate.GramAssembly.Block4.node386 line 29
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node386_check line 31
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node386_eval line 34
  10. def OAI.MUB6.Certificate.GramAssembly.Block4.node387 line 39
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node387_check line 41
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node387_eval line 44
  13. def OAI.MUB6.Certificate.GramAssembly.Block4.node388 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node388_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node388_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block4.node389 line 59
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node389_check line 61
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node389_eval line 64
  19. def OAI.MUB6.Certificate.GramAssembly.Block4.node390 line 69
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node390_check line 71
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node390_eval line 74
  22. def OAI.MUB6.Certificate.GramAssembly.Block4.node391 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node391_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node391_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block4.node392 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node392_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node392_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block4.node393 line 100
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node393_check line 102
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node393_eval line 105
  31. def OAI.MUB6.Certificate.GramAssembly.Block4.node394 line 111
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node394_check line 113
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node394_eval line 116
  34. def OAI.MUB6.Certificate.GramAssembly.Block4.node395 line 121
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node395_check line 123
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node395_eval line 126
  37. def OAI.MUB6.Certificate.GramAssembly.Block4.node396 line 132
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node396_check line 134
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node396_eval line 137
  40. def OAI.MUB6.Certificate.GramAssembly.Block4.node397 line 142
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node397_check line 144
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node397_eval line 147
  43. def OAI.MUB6.Certificate.GramAssembly.Block4.node398 line 152
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node398_check line 154
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node398_eval line 157
  46. def OAI.MUB6.Certificate.GramAssembly.Block4.node399 line 162
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node399_check line 164
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node399_eval line 167
  49. def OAI.MUB6.Certificate.GramAssembly.Block4.node400 line 172
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node400_check line 174
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node400_eval line 177
  52. def OAI.MUB6.Certificate.GramAssembly.Block4.node401 line 182
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node401_check line 184
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node401_eval line 187
  55. def OAI.MUB6.Certificate.GramAssembly.Block4.node402 line 193
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node402_check line 195
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node402_eval line 198
  58. def OAI.MUB6.Certificate.GramAssembly.Block4.node403 line 203
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node403_check line 205
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node403_eval line 208
  61. def OAI.MUB6.Certificate.GramAssembly.Block4.node404 line 213
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node404_check line 215
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node404_eval line 218
  64. def OAI.MUB6.Certificate.GramAssembly.Block4.node405 line 224
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node405_check line 226
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node405_eval line 229
  67. def OAI.MUB6.Certificate.GramAssembly.Block4.node406 line 234
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node406_check line 236
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node406_eval line 239
  70. def OAI.MUB6.Certificate.GramAssembly.Block4.node407 line 245
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node407_check line 247
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node407_eval line 250
  73. def OAI.MUB6.Certificate.GramAssembly.Block4.node408 line 255
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node408_check line 257
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node408_eval line 260
  76. def OAI.MUB6.Certificate.GramAssembly.Block4.node409 line 265
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node409_check line 267
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node409_eval line 270
  79. def OAI.MUB6.Certificate.GramAssembly.Block4.node410 line 275
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node410_check line 277
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node410_eval line 280
  82. def OAI.MUB6.Certificate.GramAssembly.Block4.node411 line 285
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node411_check line 287
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node411_eval line 290
  85. def OAI.MUB6.Certificate.GramAssembly.Block4.node412 line 296
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node412_check line 298
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node412_eval line 301
  88. def OAI.MUB6.Certificate.GramAssembly.Block4.node413 line 306
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node413_check line 308
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node413_eval line 311
  91. def OAI.MUB6.Certificate.GramAssembly.Block4.node414 line 316
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node414_check line 318
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node414_eval line 321
  94. def OAI.MUB6.Certificate.GramAssembly.Block4.node415 line 327
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node415_check line 329
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node415_eval line 332