OAI/Analysis/MutuallyUnbiased/GramFunctions/Block5.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramFunctions.Block5.shape line 7
  2. def OAI.MUB6.Certificate.GramFunctions.Block5.decimalExponent line 8
  3. def OAI.MUB6.Certificate.GramFunctions.Block5.seed0 line 10
  4. def OAI.MUB6.Certificate.GramFunctions.Block5.terms0 line 12
  5. def OAI.MUB6.Certificate.GramFunctions.Block5.form0 line 35
  6. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced0 line 37
  7. def OAI.MUB6.Certificate.GramFunctions.Block5.seed1 line 42
  8. def OAI.MUB6.Certificate.GramFunctions.Block5.terms1 line 44
  9. def OAI.MUB6.Certificate.GramFunctions.Block5.form1 line 52
  10. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced1 line 54
  11. def OAI.MUB6.Certificate.GramFunctions.Block5.seed2 line 59
  12. def OAI.MUB6.Certificate.GramFunctions.Block5.terms2 line 61
  13. def OAI.MUB6.Certificate.GramFunctions.Block5.form2 line 124
  14. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced2 line 126
  15. def OAI.MUB6.Certificate.GramFunctions.Block5.seed3 line 131
  16. def OAI.MUB6.Certificate.GramFunctions.Block5.terms3 line 133
  17. def OAI.MUB6.Certificate.GramFunctions.Block5.form3 line 141
  18. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced3 line 143
  19. def OAI.MUB6.Certificate.GramFunctions.Block5.seed4 line 148
  20. def OAI.MUB6.Certificate.GramFunctions.Block5.terms4 line 150
  21. def OAI.MUB6.Certificate.GramFunctions.Block5.form4 line 173
  22. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced4 line 175
  23. def OAI.MUB6.Certificate.GramFunctions.Block5.seed5 line 180
  24. def OAI.MUB6.Certificate.GramFunctions.Block5.terms5 line 182
  25. def OAI.MUB6.Certificate.GramFunctions.Block5.form5 line 215
  26. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced5 line 217
  27. def OAI.MUB6.Certificate.GramFunctions.Block5.seed6 line 222
  28. def OAI.MUB6.Certificate.GramFunctions.Block5.terms6 line 224
  29. def OAI.MUB6.Certificate.GramFunctions.Block5.form6 line 247
  30. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced6 line 249
  31. def OAI.MUB6.Certificate.GramFunctions.Block5.seed7 line 254
  32. def OAI.MUB6.Certificate.GramFunctions.Block5.terms7 line 256
  33. def OAI.MUB6.Certificate.GramFunctions.Block5.form7 line 279
  34. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced7 line 281
  35. def OAI.MUB6.Certificate.GramFunctions.Block5.seed8 line 286
  36. def OAI.MUB6.Certificate.GramFunctions.Block5.terms8 line 288
  37. def OAI.MUB6.Certificate.GramFunctions.Block5.form8 line 296
  38. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced8 line 298
  39. def OAI.MUB6.Certificate.GramFunctions.Block5.seed9 line 303
  40. def OAI.MUB6.Certificate.GramFunctions.Block5.terms9 line 305
  41. def OAI.MUB6.Certificate.GramFunctions.Block5.form9 line 318
  42. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced9 line 320
  43. def OAI.MUB6.Certificate.GramFunctions.Block5.seed10 line 325
  44. def OAI.MUB6.Certificate.GramFunctions.Block5.terms10 line 327
  45. def OAI.MUB6.Certificate.GramFunctions.Block5.form10 line 350
  46. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced10 line 352
  47. def OAI.MUB6.Certificate.GramFunctions.Block5.seed11 line 357
  48. def OAI.MUB6.Certificate.GramFunctions.Block5.terms11 line 359
  49. def OAI.MUB6.Certificate.GramFunctions.Block5.form11 line 422
  50. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced11 line 424
  51. def OAI.MUB6.Certificate.GramFunctions.Block5.forms line 429
  52. theorem OAI.MUB6.Certificate.GramFunctions.Block5.balanced line 432