OAI/Analysis/MutuallyUnbiased/GramAssembly/Block5Part2.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramAssembly.Block5.node64 line 8
  2. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node64_check line 10
  3. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node64_eval line 13
  4. def OAI.MUB6.Certificate.GramAssembly.Block5.node65 line 18
  5. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node65_check line 20
  6. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node65_eval line 23
  7. def OAI.MUB6.Certificate.GramAssembly.Block5.node66 line 28
  8. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node66_check line 30
  9. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node66_eval line 33
  10. def OAI.MUB6.Certificate.GramAssembly.Block5.node67 line 38
  11. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node67_check line 40
  12. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node67_eval line 43
  13. def OAI.MUB6.Certificate.GramAssembly.Block5.node68 line 49
  14. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node68_check line 51
  15. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node68_eval line 54
  16. def OAI.MUB6.Certificate.GramAssembly.Block5.node69 line 59
  17. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node69_check line 61
  18. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node69_eval line 64
  19. def OAI.MUB6.Certificate.GramAssembly.Block5.node70 line 70
  20. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node70_check line 72
  21. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node70_eval line 75
  22. def OAI.MUB6.Certificate.GramAssembly.Block5.node71 line 80
  23. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node71_check line 82
  24. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node71_eval line 85
  25. def OAI.MUB6.Certificate.GramAssembly.Block5.node72 line 90
  26. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node72_check line 92
  27. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node72_eval line 95
  28. def OAI.MUB6.Certificate.GramAssembly.Block5.node73 line 101
  29. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node73_check line 103
  30. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node73_eval line 106
  31. def OAI.MUB6.Certificate.GramAssembly.Block5.node74 line 111
  32. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node74_check line 113
  33. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node74_eval line 116
  34. def OAI.MUB6.Certificate.GramAssembly.Block5.node75 line 122
  35. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node75_check line 124
  36. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node75_eval line 127
  37. def OAI.MUB6.Certificate.GramAssembly.Block5.node76 line 132
  38. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node76_check line 134
  39. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node76_eval line 137
  40. def OAI.MUB6.Certificate.GramAssembly.Block5.node77 line 142
  41. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node77_check line 144
  42. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node77_eval line 147
  43. def OAI.MUB6.Certificate.GramAssembly.Block5.node78 line 152
  44. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node78_check line 154
  45. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node78_eval line 157
  46. def OAI.MUB6.Certificate.GramAssembly.Block5.node79 line 163
  47. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node79_check line 165
  48. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node79_eval line 168
  49. def OAI.MUB6.Certificate.GramAssembly.Block5.node80 line 173
  50. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node80_check line 175
  51. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node80_eval line 178
  52. def OAI.MUB6.Certificate.GramAssembly.Block5.node81 line 184
  53. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node81_check line 186
  54. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node81_eval line 189
  55. def OAI.MUB6.Certificate.GramAssembly.Block5.node82 line 194
  56. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node82_check line 196
  57. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node82_eval line 199
  58. def OAI.MUB6.Certificate.GramAssembly.Block5.node83 line 204
  59. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node83_check line 206
  60. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node83_eval line 209
  61. def OAI.MUB6.Certificate.GramAssembly.Block5.node84 line 215
  62. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node84_check line 217
  63. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node84_eval line 220
  64. def OAI.MUB6.Certificate.GramAssembly.Block5.node85 line 225
  65. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node85_check line 227
  66. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node85_eval line 230
  67. def OAI.MUB6.Certificate.GramAssembly.Block5.node86 line 236
  68. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node86_check line 238
  69. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node86_eval line 241
  70. def OAI.MUB6.Certificate.GramAssembly.Block5.node87 line 246
  71. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node87_check line 248
  72. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node87_eval line 251
  73. def OAI.MUB6.Certificate.GramAssembly.Block5.node88 line 256
  74. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node88_check line 258
  75. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node88_eval line 261
  76. def OAI.MUB6.Certificate.GramAssembly.Block5.node89 line 266
  77. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node89_check line 268
  78. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node89_eval line 271
  79. def OAI.MUB6.Certificate.GramAssembly.Block5.node90 line 277
  80. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node90_check line 279
  81. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node90_eval line 282
  82. def OAI.MUB6.Certificate.GramAssembly.Block5.node91 line 287
  83. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node91_check line 289
  84. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node91_eval line 292
  85. def OAI.MUB6.Certificate.GramAssembly.Block5.node92 line 298
  86. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node92_check line 300
  87. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node92_eval line 303
  88. def OAI.MUB6.Certificate.GramAssembly.Block5.node93 line 308
  89. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node93_check line 310
  90. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node93_eval line 313
  91. def OAI.MUB6.Certificate.GramAssembly.Block5.node94 line 318
  92. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node94_check line 320
  93. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node94_eval line 323
  94. def OAI.MUB6.Certificate.GramAssembly.Block5.node95 line 329
  95. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node95_check line 331
  96. theorem OAI.MUB6.Certificate.GramAssembly.Block5.node95_eval line 334