OAI/Analysis/MutuallyUnbiased/MixedSources/Rows132.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2112 line 16
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2112 line 31
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2113 line 36
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2113 line 54
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2114 line 59
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2114 line 80
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2115 line 85
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2115 line 103
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2116 line 108
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2116 line 129
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2117 line 134
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2117 line 155
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2118 line 160
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2118 line 181
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2119 line 186
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2119 line 204
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2120 line 209
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2120 line 230
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2121 line 235
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2121 line 256
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2122 line 261
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2122 line 282
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2123 line 287
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2123 line 308
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2124 line 313
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2124 line 334
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2125 line 339
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2125 line 360
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2126 line 365
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2126 line 389
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2127 line 394
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2127 line 412
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2112 line 417
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2113 line 420
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2114 line 423
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2115 line 426
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2116 line 429
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2117 line 432
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2118 line 435
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2119 line 438
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2120 line 441
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2121 line 444
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2122 line 447
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2123 line 450
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2124 line 453
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2125 line 456
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2126 line 459
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2127 line 462
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound132 line 465