OAI/Analysis/MutuallyUnbiased/GramAssembly/Block4Part13.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block4.node416 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node416_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node416_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block4.node417 line 19
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node417_check line 21
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node417_eval line 24
  7. def OAI.MUB6.Certificate.GramAssembly.Block4.node418 line 29
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node418_check line 31
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node418_eval line 34
  10. def OAI.MUB6.Certificate.GramAssembly.Block4.node419 line 39
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node419_check line 41
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node419_eval line 44
  13. def OAI.MUB6.Certificate.GramAssembly.Block4.node420 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node420_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node420_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block4.node421 line 59
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node421_check line 61
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node421_eval line 64
  19. def OAI.MUB6.Certificate.GramAssembly.Block4.node422 line 69
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node422_check line 71
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node422_eval line 74
  22. def OAI.MUB6.Certificate.GramAssembly.Block4.node423 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node423_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node423_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block4.node424 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node424_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node424_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block4.node425 line 100
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node425_check line 102
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node425_eval line 105
  31. def OAI.MUB6.Certificate.GramAssembly.Block4.node426 line 111
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node426_check line 113
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node426_eval line 116
  34. def OAI.MUB6.Certificate.GramAssembly.Block4.node427 line 121
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node427_check line 123
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node427_eval line 126
  37. def OAI.MUB6.Certificate.GramAssembly.Block4.node428 line 132
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node428_check line 134
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node428_eval line 137
  40. def OAI.MUB6.Certificate.GramAssembly.Block4.node429 line 142
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node429_check line 144
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node429_eval line 147
  43. def OAI.MUB6.Certificate.GramAssembly.Block4.node430 line 152
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node430_check line 154
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node430_eval line 157
  46. def OAI.MUB6.Certificate.GramAssembly.Block4.node431 line 162
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node431_check line 164
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node431_eval line 167
  49. def OAI.MUB6.Certificate.GramAssembly.Block4.node432 line 172
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node432_check line 174
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node432_eval line 177
  52. def OAI.MUB6.Certificate.GramAssembly.Block4.node433 line 183
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node433_check line 185
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node433_eval line 188
  55. def OAI.MUB6.Certificate.GramAssembly.Block4.node434 line 193
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node434_check line 195
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node434_eval line 198
  58. def OAI.MUB6.Certificate.GramAssembly.Block4.node435 line 203
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node435_check line 205
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node435_eval line 208
  61. def OAI.MUB6.Certificate.GramAssembly.Block4.node436 line 214
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node436_check line 216
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node436_eval line 219
  64. def OAI.MUB6.Certificate.GramAssembly.Block4.node437 line 224
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node437_check line 226
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node437_eval line 229
  67. def OAI.MUB6.Certificate.GramAssembly.Block4.node438 line 235
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node438_check line 237
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node438_eval line 240
  70. def OAI.MUB6.Certificate.GramAssembly.Block4.node439 line 245
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node439_check line 247
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node439_eval line 250
  73. def OAI.MUB6.Certificate.GramAssembly.Block4.node440 line 255
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node440_check line 257
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node440_eval line 260
  76. def OAI.MUB6.Certificate.GramAssembly.Block4.node441 line 265
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node441_check line 267
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node441_eval line 270
  79. def OAI.MUB6.Certificate.GramAssembly.Block4.node442 line 275
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node442_check line 277
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node442_eval line 280
  82. def OAI.MUB6.Certificate.GramAssembly.Block4.node443 line 285
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node443_check line 287
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node443_eval line 290
  85. def OAI.MUB6.Certificate.GramAssembly.Block4.node444 line 296
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node444_check line 298
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node444_eval line 301
  88. def OAI.MUB6.Certificate.GramAssembly.Block4.node445 line 306
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node445_check line 308
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node445_eval line 311
  91. def OAI.MUB6.Certificate.GramAssembly.Block4.node446 line 316
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node446_check line 318
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node446_eval line 321
  94. def OAI.MUB6.Certificate.GramAssembly.Block4.node447 line 327
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node447_check line 329
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block4.node447_eval line 332