OAI/Analysis/MutuallyUnbiased/MixedSources/Rows65.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1040 line 34
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1040 line 55
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1041 line 60
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1041 line 81
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1042 line 86
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1042 line 107
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1043 line 112
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1043 line 133
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1044 line 138
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1044 line 162
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1045 line 167
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1045 line 191
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1046 line 196
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1046 line 220
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1047 line 225
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1047 line 249
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1048 line 254
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1048 line 278
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1049 line 283
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1049 line 307
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1050 line 312
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1050 line 336
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1051 line 341
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1051 line 365
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1052 line 370
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1052 line 394
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1053 line 399
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1053 line 423
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1054 line 428
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1054 line 452
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1055 line 457
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1055 line 481
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1040 line 486
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1041 line 489
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1042 line 492
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1043 line 495
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1044 line 498
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1045 line 501
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1046 line 504
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1047 line 507
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1048 line 510
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1049 line 513
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1050 line 516
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1051 line 519
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1052 line 522
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1053 line 525
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1054 line 528
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1055 line 531
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound65 line 534