OAI/Analysis/MutuallyUnbiased/PairPolynomial/Assembly.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.PairTargetSemantics.sum_grid_polynomial line 9
  2. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at0 line 14
  3. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at1 line 15
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at2 line 16
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at3 line 17
  6. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at4 line 18
  7. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at5 line 19
  8. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at6 line 20
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at7 line 21
  10. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at8 line 22
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at9 line 23
  12. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at10 line 24
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at11 line 25
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at12 line 26
  15. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at13 line 27
  16. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at14 line 28
  17. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at15 line 29
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at16 line 30
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at17 line 31
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at18 line 32
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at19 line 33
  22. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at20 line 34
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at21 line 35
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at22 line 36
  25. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at23 line 37
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_at24 line 38
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at0 line 40
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at1 line 41
  29. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at2 line 42
  30. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at3 line 43
  31. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at4 line 44
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at5 line 45
  33. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at6 line 46
  34. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at7 line 47
  35. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at8 line 48
  36. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at9 line 49
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at10 line 50
  38. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at11 line 51
  39. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at12 line 52
  40. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at13 line 53
  41. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at14 line 54
  42. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at15 line 55
  43. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at16 line 56
  44. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at17 line 57
  45. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at18 line 58
  46. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at19 line 59
  47. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at20 line 60
  48. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at21 line 61
  49. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at22 line 62
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at23 line 63
  51. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at24 line 64
  52. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms0_at25 line 65
  53. theorem OAI.MUB6.Certificate.PairTargetSemantics.sum_terms0 line 66
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.pair_polynomial0 line 72
  55. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at0 line 82
  56. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at1 line 83
  57. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at2 line 84
  58. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at3 line 85
  59. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at4 line 86
  60. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at5 line 87
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at6 line 88
  62. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at7 line 89
  63. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at8 line 90
  64. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at9 line 91
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at10 line 92
  66. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at11 line 93
  67. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at12 line 94
  68. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at13 line 95
  69. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at14 line 96
  70. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at15 line 97
  71. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at16 line 98
  72. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at17 line 99
  73. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at18 line 100
  74. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at19 line 101
  75. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at20 line 102
  76. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at21 line 103
  77. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at22 line 104
  78. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at23 line 105
  79. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at24 line 106
  80. theorem OAI.MUB6.Certificate.PairTargetSemantics.terms1_at25 line 107
  81. theorem OAI.MUB6.Certificate.PairTargetSemantics.sum_terms1 line 108
  82. theorem OAI.MUB6.Certificate.PairTargetSemantics.pair_polynomial1 line 114