OAI/Analysis/MutuallyUnbiased/MixedSources/Rows129.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2064 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2064 line 137
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2065 line 142
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2065 line 238
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2066 line 243
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2066 line 312
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2067 line 317
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2067 line 386
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2068 line 391
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2068 line 460
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2069 line 465
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2069 line 558
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2070 line 563
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2070 line 656
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2071 line 661
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2071 line 730
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2072 line 735
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2072 line 804
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2073 line 809
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2073 line 905
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2074 line 910
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2074 line 1006
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2075 line 1011
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2075 line 1059
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2076 line 1064
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2076 line 1112
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2077 line 1117
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2077 line 1183
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2078 line 1188
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2078 line 1257
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2079 line 1262
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2079 line 1331
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2064 line 1336
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2065 line 1339
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2066 line 1342
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2067 line 1345
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2068 line 1348
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2069 line 1351
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2070 line 1354
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2071 line 1357
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2072 line 1360
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2073 line 1363
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2074 line 1366
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2075 line 1369
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2076 line 1372
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2077 line 1375
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2078 line 1378
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2079 line 1381
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound129 line 1384