OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound54.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3456 line 68
  2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3456 line 74
  3. theorem OAI.MUB6.Certificate.PairSemantics.sound3456 line 76
  4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3457 line 116
  5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3457 line 122
  6. theorem OAI.MUB6.Certificate.PairSemantics.sound3457 line 124
  7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3458 line 164
  8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3458 line 170
  9. theorem OAI.MUB6.Certificate.PairSemantics.sound3458 line 172
  10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3459 line 212
  11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3459 line 218
  12. theorem OAI.MUB6.Certificate.PairSemantics.sound3459 line 220
  13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3460 line 260
  14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3460 line 266
  15. theorem OAI.MUB6.Certificate.PairSemantics.sound3460 line 268
  16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3461 line 308
  17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3461 line 314
  18. theorem OAI.MUB6.Certificate.PairSemantics.sound3461 line 316
  19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3462 line 356
  20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3462 line 362
  21. theorem OAI.MUB6.Certificate.PairSemantics.sound3462 line 364
  22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3463 line 404
  23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3463 line 410
  24. theorem OAI.MUB6.Certificate.PairSemantics.sound3463 line 412
  25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3464 line 452
  26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3464 line 458
  27. theorem OAI.MUB6.Certificate.PairSemantics.sound3464 line 460
  28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3465 line 500
  29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3465 line 506
  30. theorem OAI.MUB6.Certificate.PairSemantics.sound3465 line 508
  31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3466 line 548
  32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3466 line 554
  33. theorem OAI.MUB6.Certificate.PairSemantics.sound3466 line 556
  34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3467 line 596
  35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3467 line 602
  36. theorem OAI.MUB6.Certificate.PairSemantics.sound3467 line 604
  37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3468 line 644
  38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3468 line 650
  39. theorem OAI.MUB6.Certificate.PairSemantics.sound3468 line 652