OAI/Analysis/MutuallyUnbiased/MixedSources/Rows90.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1440 line 40
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1440 line 67
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1441 line 72
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1441 line 162
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1442 line 167
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1442 line 257
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1443 line 262
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1443 line 289
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1444 line 294
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1444 line 318
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1445 line 323
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1445 line 350
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1446 line 355
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1446 line 379
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1447 line 384
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1447 line 411
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1448 line 416
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1448 line 437
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1449 line 442
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1449 line 466
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1450 line 471
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1450 line 492
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1451 line 497
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1451 line 521
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1452 line 526
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1452 line 550
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1453 line 555
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1453 line 582
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1454 line 587
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1454 line 614
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1455 line 619
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1455 line 643
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1440 line 648
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1441 line 651
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1442 line 654
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1443 line 657
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1444 line 660
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1445 line 663
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1446 line 666
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1447 line 669
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1448 line 672
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1449 line 675
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1450 line 678
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1451 line 681
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1452 line 684
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1453 line 687
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1454 line 690
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1455 line 693
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound90 line 696