OAI/Analysis/MutuallyUnbiased/MixedSources/Rows83.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1328 line 33
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1328 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1329 line 62
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1329 line 83
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1330 line 88
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1330 line 112
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1331 line 117
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1331 line 144
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1332 line 149
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1332 line 173
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1333 line 178
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1333 line 199
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1334 line 204
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1334 line 228
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1335 line 233
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1335 line 302
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1336 line 307
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1336 line 376
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1337 line 381
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1337 line 405
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1338 line 410
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1338 line 434
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1339 line 439
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1339 line 463
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1340 line 468
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1340 line 534
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1341 line 539
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1341 line 569
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1342 line 574
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1342 line 598
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1343 line 603
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1343 line 627
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1328 line 632
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1329 line 635
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1330 line 638
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1331 line 641
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1332 line 644
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1333 line 647
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1334 line 650
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1335 line 653
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1336 line 656
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1337 line 659
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1338 line 662
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1339 line 665
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1340 line 668
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1341 line 671
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1342 line 674
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1343 line 677
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound83 line 680