OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical8.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw128 line 13
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw128step0 line 15
  3. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical128 line 17
  4. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw129 line 27
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw129step0 line 29
  6. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical129 line 31
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw130 line 41
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw130step0 line 43
  9. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw130step1 line 45
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw130step2 line 47
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw130step3 line 49
  12. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical130 line 51
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131 line 80
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131step0 line 82
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131step1 line 84
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131step2 line 86
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131step3 line 88
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131step4 line 90
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw131step5 line 92
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical131 line 94
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw132 line 134
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw132step0 line 136
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical132 line 138
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw133 line 148
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw133step0 line 150
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw133step1 line 152
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical133 line 154
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw134 line 169
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw134step0 line 171
  30. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical134 line 173
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw135 line 183
  32. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw135step0 line 185
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw135step1 line 187
  34. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical135 line 189
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw136 line 204
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw136step0 line 206
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical136 line 208