OAI/Analysis/MutuallyUnbiased/MixedSources/Rows75.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1200 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1200 line 60
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1201 line 65
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1201 line 89
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1202 line 94
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1202 line 118
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1203 line 123
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1203 line 147
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1204 line 152
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1204 line 176
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1205 line 181
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1205 line 250
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1206 line 255
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1206 line 324
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1207 line 329
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1207 line 356
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1208 line 361
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1208 line 388
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1209 line 393
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1209 line 417
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1210 line 422
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1210 line 446
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1211 line 451
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1211 line 475
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1212 line 480
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1212 line 504
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1213 line 509
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1213 line 533
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1214 line 538
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1214 line 562
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1215 line 567
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1215 line 591
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1200 line 596
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1201 line 599
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1202 line 602
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1203 line 605
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1204 line 608
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1205 line 611
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1206 line 614
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1207 line 617
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1208 line 620
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1209 line 623
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1210 line 626
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1211 line 629
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1212 line 632
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1213 line 635
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1214 line 638
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1215 line 641
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound75 line 644