OAI/Analysis/MutuallyUnbiased/MixedSources/Rows20.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero320 line 44
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound320 line 68
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero321 line 73
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound321 line 97
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero322 line 102
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound322 line 126
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero323 line 131
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound323 line 155
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero324 line 160
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound324 line 187
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero325 line 192
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound325 line 213
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero326 line 218
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound326 line 287
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero327 line 292
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound327 line 361
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero328 line 366
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound328 line 435
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero329 line 440
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound329 line 464
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero330 line 469
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound330 line 493
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero331 line 498
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound331 line 522
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero332 line 527
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound332 line 551
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero333 line 556
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound333 line 583
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero334 line 588
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound334 line 612
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero335 line 617
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound335 line 686
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt320 line 691
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt321 line 694
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt322 line 697
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt323 line 700
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt324 line 703
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt325 line 706
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt326 line 709
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt327 line 712
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt328 line 715
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt329 line 718
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt330 line 721
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt331 line 724
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt332 line 727
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt333 line 730
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt334 line 733
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt335 line 736
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound20 line 739