OAI/Analysis/MutuallyUnbiased/GramAssembly/Block3Part0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block3.node0 line 7
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node0_check line 9
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node0_eval line 12
  4. def OAI.MUB6.Certificate.GramAssembly.Block3.node1 line 17
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node1_check line 19
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node1_eval line 22
  7. def OAI.MUB6.Certificate.GramAssembly.Block3.node2 line 28
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node2_check line 30
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node2_eval line 33
  10. def OAI.MUB6.Certificate.GramAssembly.Block3.node3 line 38
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node3_check line 40
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node3_eval line 43
  13. def OAI.MUB6.Certificate.GramAssembly.Block3.node4 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node4_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node4_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block3.node5 line 59
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node5_check line 61
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node5_eval line 64
  19. def OAI.MUB6.Certificate.GramAssembly.Block3.node6 line 69
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node6_check line 71
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node6_eval line 74
  22. def OAI.MUB6.Certificate.GramAssembly.Block3.node7 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node7_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node7_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block3.node8 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node8_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node8_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block3.node9 line 100
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node9_check line 102
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node9_eval line 105
  31. def OAI.MUB6.Certificate.GramAssembly.Block3.node10 line 110
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node10_check line 112
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node10_eval line 115
  34. def OAI.MUB6.Certificate.GramAssembly.Block3.node11 line 120
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node11_check line 122
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node11_eval line 125
  37. def OAI.MUB6.Certificate.GramAssembly.Block3.node12 line 130
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node12_check line 132
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node12_eval line 135
  40. def OAI.MUB6.Certificate.GramAssembly.Block3.node13 line 140
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node13_check line 142
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node13_eval line 145
  43. def OAI.MUB6.Certificate.GramAssembly.Block3.node14 line 151
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node14_check line 153
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node14_eval line 156
  46. def OAI.MUB6.Certificate.GramAssembly.Block3.node15 line 161
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node15_check line 163
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node15_eval line 166
  49. def OAI.MUB6.Certificate.GramAssembly.Block3.node16 line 171
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node16_check line 173
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node16_eval line 176
  52. def OAI.MUB6.Certificate.GramAssembly.Block3.node17 line 181
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node17_check line 183
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node17_eval line 186
  55. def OAI.MUB6.Certificate.GramAssembly.Block3.node18 line 191
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node18_check line 193
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node18_eval line 196
  58. def OAI.MUB6.Certificate.GramAssembly.Block3.node19 line 201
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node19_check line 203
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node19_eval line 206
  61. def OAI.MUB6.Certificate.GramAssembly.Block3.node20 line 212
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node20_check line 214
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node20_eval line 217
  64. def OAI.MUB6.Certificate.GramAssembly.Block3.node21 line 222
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node21_check line 224
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node21_eval line 227
  67. def OAI.MUB6.Certificate.GramAssembly.Block3.node22 line 232
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node22_check line 234
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node22_eval line 237
  70. def OAI.MUB6.Certificate.GramAssembly.Block3.node23 line 242
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node23_check line 244
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node23_eval line 247
  73. def OAI.MUB6.Certificate.GramAssembly.Block3.node24 line 252
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node24_check line 254
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node24_eval line 257
  76. def OAI.MUB6.Certificate.GramAssembly.Block3.node25 line 262
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node25_check line 264
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node25_eval line 267
  79. def OAI.MUB6.Certificate.GramAssembly.Block3.node26 line 272
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node26_check line 274
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node26_eval line 277
  82. def OAI.MUB6.Certificate.GramAssembly.Block3.node27 line 282
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node27_check line 284
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node27_eval line 287
  85. def OAI.MUB6.Certificate.GramAssembly.Block3.node28 line 293
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node28_check line 295
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node28_eval line 298
  88. def OAI.MUB6.Certificate.GramAssembly.Block3.node29 line 303
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node29_check line 305
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node29_eval line 308
  91. def OAI.MUB6.Certificate.GramAssembly.Block3.node30 line 314
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node30_check line 316
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node30_eval line 319
  94. def OAI.MUB6.Certificate.GramAssembly.Block3.node31 line 324
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node31_check line 326
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block3.node31_eval line 329