OAI/Analysis/MutuallyUnbiased/PairMerge/Block11.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairData.pairMerged352 line 9
  2. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck352 line 11
  3. theorem OAI.MUB6.Certificate.PairData.pairMergedZero352 line 13
  4. def OAI.MUB6.Certificate.PairData.pairMerged353 line 19
  5. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck353 line 21
  6. theorem OAI.MUB6.Certificate.PairData.pairMergedZero353 line 23
  7. def OAI.MUB6.Certificate.PairData.pairMerged354 line 28
  8. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck354 line 30
  9. theorem OAI.MUB6.Certificate.PairData.pairMergedZero354 line 32
  10. def OAI.MUB6.Certificate.PairData.pairMerged355 line 37
  11. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck355 line 39
  12. theorem OAI.MUB6.Certificate.PairData.pairMergedZero355 line 41
  13. def OAI.MUB6.Certificate.PairData.pairMerged356 line 47
  14. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck356 line 49
  15. theorem OAI.MUB6.Certificate.PairData.pairMergedZero356 line 51
  16. def OAI.MUB6.Certificate.PairData.pairMerged357 line 57
  17. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck357 line 59
  18. theorem OAI.MUB6.Certificate.PairData.pairMergedZero357 line 61
  19. def OAI.MUB6.Certificate.PairData.pairMerged358 line 67
  20. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck358 line 69
  21. theorem OAI.MUB6.Certificate.PairData.pairMergedZero358 line 71
  22. def OAI.MUB6.Certificate.PairData.pairMerged359 line 77
  23. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck359 line 79
  24. theorem OAI.MUB6.Certificate.PairData.pairMergedZero359 line 81
  25. def OAI.MUB6.Certificate.PairData.pairMerged360 line 87
  26. theorem OAI.MUB6.Certificate.PairData.pairMergeCheck360 line 89
  27. theorem OAI.MUB6.Certificate.PairData.pairMergedZero360 line 91