OAI/Analysis/MutuallyUnbiased/MixedSources/Rows12.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero192 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound192 line 63
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero193 line 68
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound193 line 95
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero194 line 100
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound194 line 127
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero195 line 132
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound195 line 156
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero196 line 161
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound196 line 185
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero197 line 190
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound197 line 214
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero198 line 219
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound198 line 288
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero199 line 293
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound199 line 362
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero200 line 367
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound200 line 391
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero201 line 396
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound201 line 420
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero202 line 425
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound202 line 449
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero203 line 454
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound203 line 478
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero204 line 483
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound204 line 510
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero205 line 515
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound205 line 542
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero206 line 547
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound206 line 571
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero207 line 576
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound207 line 645
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt192 line 650
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt193 line 653
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt194 line 656
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt195 line 659
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt196 line 662
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt197 line 665
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt198 line 668
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt199 line 671
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt200 line 674
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt201 line 677
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt202 line 680
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt203 line 683
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt204 line 686
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt205 line 689
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt206 line 692
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt207 line 695
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound12 line 698