OAI/Analysis/MutuallyUnbiased/MixedSources/Rows24.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero384 line 45
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound384 line 72
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero385 line 77
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound385 line 98
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero386 line 103
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound386 line 127
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero387 line 132
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound387 line 153
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero388 line 158
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound388 line 227
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero389 line 232
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound389 line 256
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero390 line 261
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound390 line 285
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero391 line 290
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound391 line 359
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero392 line 364
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound392 line 433
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero393 line 438
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound393 line 456
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero394 line 461
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound394 line 485
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero395 line 490
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound395 line 559
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero396 line 564
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound396 line 633
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero397 line 638
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound397 line 662
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero398 line 667
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound398 line 691
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero399 line 696
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound399 line 723
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt384 line 728
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt385 line 731
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt386 line 734
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt387 line 737
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt388 line 740
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt389 line 743
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt390 line 746
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt391 line 749
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt392 line 752
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt393 line 755
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt394 line 758
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt395 line 761
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt396 line 764
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt397 line 767
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt398 line 770
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt399 line 773
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound24 line 776