OAI/Analysis/MutuallyUnbiased/MixedSources/Rows14.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero224 line 40
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound224 line 67
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero225 line 72
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound225 line 99
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero226 line 104
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound226 line 200
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero227 line 205
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound227 line 232
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero228 line 237
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound228 line 264
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero229 line 269
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound229 line 296
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero230 line 301
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound230 line 328
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero231 line 333
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound231 line 360
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero232 line 365
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound232 line 392
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero233 line 397
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound233 line 421
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero234 line 426
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound234 line 453
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero235 line 458
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound235 line 485
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero236 line 490
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound236 line 583
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero237 line 588
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound237 line 615
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero238 line 620
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound238 line 647
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero239 line 652
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound239 line 676
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt224 line 681
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt225 line 684
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt226 line 687
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt227 line 690
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt228 line 693
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt229 line 696
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt230 line 699
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt231 line 702
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt232 line 705
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt233 line 708
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt234 line 711
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt235 line 714
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt236 line 717
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt237 line 720
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt238 line 723
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt239 line 726
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound14 line 729