OAI/Analysis/MutuallyUnbiased/MixedSources/Rows11.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero176 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound176 line 86
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero177 line 91
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound177 line 112
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero178 line 117
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound178 line 138
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero179 line 143
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound179 line 167
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero180 line 172
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound180 line 196
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero181 line 201
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound181 line 222
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero182 line 227
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound182 line 248
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero183 line 253
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound183 line 274
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero184 line 279
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound184 line 324
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero185 line 329
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound185 line 350
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero186 line 355
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound186 line 376
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero187 line 381
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound187 line 402
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero188 line 407
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound188 line 476
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero189 line 481
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound189 line 505
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero190 line 510
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound190 line 534
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero191 line 539
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound191 line 563
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt176 line 568
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt177 line 571
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt178 line 574
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt179 line 577
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt180 line 580
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt181 line 583
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt182 line 586
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt183 line 589
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt184 line 592
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt185 line 595
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt186 line 598
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt187 line 601
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt188 line 604
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt189 line 607
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt190 line 610
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt191 line 613
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound11 line 616