OAI/Analysis/MutuallyUnbiased/MixedSources/Rows89.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1424 line 46
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1424 line 115
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1425 line 120
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1425 line 144
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1426 line 149
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1426 line 170
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1427 line 175
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1427 line 202
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1428 line 207
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1428 line 276
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1429 line 281
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1429 line 350
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1430 line 355
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1430 line 424
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1431 line 429
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1431 line 453
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1432 line 458
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1432 line 482
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1433 line 487
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1433 line 556
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1434 line 561
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1434 line 630
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1435 line 635
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1435 line 704
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1436 line 709
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1436 line 802
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1437 line 807
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1437 line 903
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1438 line 908
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1438 line 1001
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1439 line 1006
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1439 line 1033
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1424 line 1038
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1425 line 1041
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1426 line 1044
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1427 line 1047
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1428 line 1050
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1429 line 1053
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1430 line 1056
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1431 line 1059
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1432 line 1062
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1433 line 1065
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1434 line 1068
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1435 line 1071
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1436 line 1074
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1437 line 1077
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1438 line 1080
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1439 line 1083
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound89 line 1086