OAI/Analysis/MutuallyUnbiased/MixedSources/Rows17.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero272 line 46
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound272 line 70
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero273 line 75
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound273 line 99
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero274 line 104
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound274 line 131
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero275 line 136
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound275 line 160
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero276 line 165
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound276 line 192
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero277 line 197
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound277 line 221
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero278 line 226
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound278 line 253
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero279 line 258
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound279 line 285
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero280 line 290
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound280 line 317
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero281 line 322
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound281 line 418
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero282 line 423
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound282 line 519
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero283 line 524
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound283 line 545
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero284 line 550
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound284 line 577
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero285 line 582
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound285 line 609
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero286 line 614
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound286 line 710
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero287 line 715
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound287 line 811
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt272 line 816
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt273 line 819
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt274 line 822
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt275 line 825
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt276 line 828
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt277 line 831
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt278 line 834
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt279 line 837
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt280 line 840
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt281 line 843
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt282 line 846
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt283 line 849
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt284 line 852
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt285 line 855
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt286 line 858
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt287 line 861
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound17 line 864