OAI/Analysis/MutuallyUnbiased/PairPolynomial/Grid.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.termGrid line 10
  2. def OAI.MUB6.Certificate.PairTargetSemantics.pairSummand line 13
  3. theorem OAI.MUB6.Certificate.PairTargetSemantics.pairSummand_sum line 19
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid0 line 22
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid1 line 28
  6. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid2 line 35
  7. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid3 line 42
  8. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid4 line 49
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid5 line 56
  10. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid6 line 63
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid7 line 70
  12. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid8 line 77
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid9 line 84
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid10 line 91
  15. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid11 line 97
  16. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid12 line 104
  17. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid13 line 111
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid14 line 118
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid15 line 125
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid16 line 131
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid17 line 138
  22. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid18 line 145
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid19 line 152
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid20 line 159
  25. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid21 line 165
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid22 line 172
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid23 line 179
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.grid24 line 186
  29. theorem OAI.MUB6.Certificate.PairTargetSemantics.termGrid_polynomial line 193