OAI/Analysis/MutuallyUnbiased/MixedSources/Rows87.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1392 line 30
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1392 line 54
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1393 line 59
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1393 line 83
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1394 line 88
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1394 line 112
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1395 line 117
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1395 line 144
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1396 line 149
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1396 line 173
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1397 line 178
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1397 line 205
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1398 line 210
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1398 line 234
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1399 line 239
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1399 line 266
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1400 line 271
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1400 line 298
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1401 line 303
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1401 line 327
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1402 line 332
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1402 line 353
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1403 line 358
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1403 line 385
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1404 line 390
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1404 line 414
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1405 line 419
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1405 line 443
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1406 line 448
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1406 line 472
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1407 line 477
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1407 line 501
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1392 line 506
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1393 line 509
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1394 line 512
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1395 line 515
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1396 line 518
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1397 line 521
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1398 line 524
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1399 line 527
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1400 line 530
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1401 line 533
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1402 line 536
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1403 line 539
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1404 line 542
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1405 line 545
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1406 line 548
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1407 line 551
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound87 line 554