OAI/Analysis/MutuallyUnbiased/MixedSources/Rows62.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero992 line 34
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound992 line 58
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero993 line 63
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound993 line 78
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero994 line 83
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound994 line 104
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero995 line 109
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound995 line 130
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero996 line 135
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound996 line 153
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero997 line 158
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound997 line 182
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero998 line 187
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound998 line 208
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero999 line 213
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound999 line 237
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1000 line 242
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1000 line 266
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1001 line 271
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1001 line 295
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1002 line 300
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1002 line 318
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1003 line 323
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1003 line 347
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1004 line 352
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1004 line 376
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1005 line 381
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1005 line 405
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1006 line 410
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1006 line 434
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1007 line 439
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1007 line 460
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt992 line 465
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt993 line 468
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt994 line 471
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt995 line 474
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt996 line 477
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt997 line 480
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt998 line 483
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt999 line 486
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1000 line 489
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1001 line 492
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1002 line 495
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1003 line 498
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1004 line 501
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1005 line 504
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1006 line 507
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1007 line 510
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound62 line 513