OAI/Analysis/MutuallyUnbiased/GramFunctions/Block2.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.GramFunctions.Block2.shape line 7
  2. def OAI.MUB6.Certificate.GramFunctions.Block2.decimalExponent line 8
  3. def OAI.MUB6.Certificate.GramFunctions.Block2.seed0 line 10
  4. def OAI.MUB6.Certificate.GramFunctions.Block2.terms0 line 12
  5. def OAI.MUB6.Certificate.GramFunctions.Block2.form0 line 55
  6. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced0 line 57
  7. def OAI.MUB6.Certificate.GramFunctions.Block2.seed1 line 62
  8. def OAI.MUB6.Certificate.GramFunctions.Block2.terms1 line 64
  9. def OAI.MUB6.Certificate.GramFunctions.Block2.form1 line 107
  10. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced1 line 109
  11. def OAI.MUB6.Certificate.GramFunctions.Block2.seed2 line 114
  12. def OAI.MUB6.Certificate.GramFunctions.Block2.terms2 line 116
  13. def OAI.MUB6.Certificate.GramFunctions.Block2.form2 line 159
  14. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced2 line 161
  15. def OAI.MUB6.Certificate.GramFunctions.Block2.seed3 line 166
  16. def OAI.MUB6.Certificate.GramFunctions.Block2.terms3 line 168
  17. def OAI.MUB6.Certificate.GramFunctions.Block2.form3 line 201
  18. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced3 line 203
  19. def OAI.MUB6.Certificate.GramFunctions.Block2.seed4 line 208
  20. def OAI.MUB6.Certificate.GramFunctions.Block2.terms4 line 210
  21. def OAI.MUB6.Certificate.GramFunctions.Block2.form4 line 243
  22. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced4 line 245
  23. def OAI.MUB6.Certificate.GramFunctions.Block2.seed5 line 250
  24. def OAI.MUB6.Certificate.GramFunctions.Block2.terms5 line 252
  25. def OAI.MUB6.Certificate.GramFunctions.Block2.form5 line 295
  26. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced5 line 297
  27. def OAI.MUB6.Certificate.GramFunctions.Block2.seed6 line 302
  28. def OAI.MUB6.Certificate.GramFunctions.Block2.terms6 line 304
  29. def OAI.MUB6.Certificate.GramFunctions.Block2.form6 line 347
  30. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced6 line 349
  31. def OAI.MUB6.Certificate.GramFunctions.Block2.seed7 line 354
  32. def OAI.MUB6.Certificate.GramFunctions.Block2.terms7 line 356
  33. def OAI.MUB6.Certificate.GramFunctions.Block2.form7 line 399
  34. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced7 line 401
  35. def OAI.MUB6.Certificate.GramFunctions.Block2.seed8 line 406
  36. def OAI.MUB6.Certificate.GramFunctions.Block2.terms8 line 408
  37. def OAI.MUB6.Certificate.GramFunctions.Block2.form8 line 451
  38. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced8 line 453
  39. def OAI.MUB6.Certificate.GramFunctions.Block2.seed9 line 458
  40. def OAI.MUB6.Certificate.GramFunctions.Block2.terms9 line 460
  41. def OAI.MUB6.Certificate.GramFunctions.Block2.form9 line 493
  42. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced9 line 495
  43. def OAI.MUB6.Certificate.GramFunctions.Block2.seed10 line 500
  44. def OAI.MUB6.Certificate.GramFunctions.Block2.terms10 line 502
  45. def OAI.MUB6.Certificate.GramFunctions.Block2.form10 line 535
  46. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced10 line 537
  47. def OAI.MUB6.Certificate.GramFunctions.Block2.forms line 542
  48. theorem OAI.MUB6.Certificate.GramFunctions.Block2.balanced line 545