OAI/Analysis/MutuallyUnbiased/GramAssembly/Block5Part0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block5.node0 line 7
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node0_check line 9
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node0_eval line 12
  4. def OAI.MUB6.Certificate.GramAssembly.Block5.node1 line 17
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node1_check line 19
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node1_eval line 22
  7. def OAI.MUB6.Certificate.GramAssembly.Block5.node2 line 28
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node2_check line 30
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node2_eval line 33
  10. def OAI.MUB6.Certificate.GramAssembly.Block5.node3 line 38
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node3_check line 40
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node3_eval line 43
  13. def OAI.MUB6.Certificate.GramAssembly.Block5.node4 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node4_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node4_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block5.node5 line 59
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node5_check line 61
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node5_eval line 64
  19. def OAI.MUB6.Certificate.GramAssembly.Block5.node6 line 69
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node6_check line 71
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node6_eval line 74
  22. def OAI.MUB6.Certificate.GramAssembly.Block5.node7 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node7_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node7_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block5.node8 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node8_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node8_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block5.node9 line 101
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node9_check line 103
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node9_eval line 106
  31. def OAI.MUB6.Certificate.GramAssembly.Block5.node10 line 111
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node10_check line 113
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node10_eval line 116
  34. def OAI.MUB6.Certificate.GramAssembly.Block5.node11 line 121
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node11_check line 123
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node11_eval line 126
  37. def OAI.MUB6.Certificate.GramAssembly.Block5.node12 line 131
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node12_check line 133
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node12_eval line 136
  40. def OAI.MUB6.Certificate.GramAssembly.Block5.node13 line 142
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node13_check line 144
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node13_eval line 147
  43. def OAI.MUB6.Certificate.GramAssembly.Block5.node14 line 152
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node14_check line 154
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node14_eval line 157
  46. def OAI.MUB6.Certificate.GramAssembly.Block5.node15 line 163
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node15_check line 165
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node15_eval line 168
  49. def OAI.MUB6.Certificate.GramAssembly.Block5.node16 line 173
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node16_check line 175
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node16_eval line 178
  52. def OAI.MUB6.Certificate.GramAssembly.Block5.node17 line 183
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node17_check line 185
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node17_eval line 188
  55. def OAI.MUB6.Certificate.GramAssembly.Block5.node18 line 194
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node18_check line 196
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node18_eval line 199
  58. def OAI.MUB6.Certificate.GramAssembly.Block5.node19 line 204
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node19_check line 206
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node19_eval line 209
  61. def OAI.MUB6.Certificate.GramAssembly.Block5.node20 line 215
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node20_check line 217
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node20_eval line 220
  64. def OAI.MUB6.Certificate.GramAssembly.Block5.node21 line 225
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node21_check line 227
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node21_eval line 230
  67. def OAI.MUB6.Certificate.GramAssembly.Block5.node22 line 235
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node22_check line 237
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node22_eval line 240
  70. def OAI.MUB6.Certificate.GramAssembly.Block5.node23 line 245
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node23_check line 247
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node23_eval line 250
  73. def OAI.MUB6.Certificate.GramAssembly.Block5.node24 line 256
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node24_check line 258
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node24_eval line 261
  76. def OAI.MUB6.Certificate.GramAssembly.Block5.node25 line 266
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node25_check line 268
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node25_eval line 271
  79. def OAI.MUB6.Certificate.GramAssembly.Block5.node26 line 277
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node26_check line 279
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node26_eval line 282
  82. def OAI.MUB6.Certificate.GramAssembly.Block5.node27 line 287
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node27_check line 289
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node27_eval line 292
  85. def OAI.MUB6.Certificate.GramAssembly.Block5.node28 line 297
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node28_check line 299
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node28_eval line 302
  88. def OAI.MUB6.Certificate.GramAssembly.Block5.node29 line 308
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node29_check line 310
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node29_eval line 313
  91. def OAI.MUB6.Certificate.GramAssembly.Block5.node30 line 318
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node30_check line 320
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node30_eval line 323
  94. def OAI.MUB6.Certificate.GramAssembly.Block5.node31 line 329
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node31_check line 331
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node31_eval line 334