OAI/Analysis/MutuallyUnbiased/MixedSources/Rows74.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1184 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1184 line 68
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1185 line 73
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1185 line 100
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1186 line 105
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1186 line 132
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1187 line 137
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1187 line 164
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1188 line 169
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1188 line 196
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1189 line 201
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1189 line 228
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1190 line 233
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1190 line 260
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1191 line 265
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1191 line 310
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1192 line 315
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1192 line 360
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1193 line 365
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1193 line 389
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1194 line 394
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1194 line 439
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1195 line 444
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1195 line 489
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1196 line 494
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1196 line 539
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1197 line 544
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1197 line 589
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1198 line 594
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1198 line 639
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1199 line 644
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1199 line 665
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1184 line 670
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1185 line 673
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1186 line 676
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1187 line 679
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1188 line 682
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1189 line 685
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1190 line 688
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1191 line 691
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1192 line 694
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1193 line 697
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1194 line 700
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1195 line 703
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1196 line 706
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1197 line 709
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1198 line 712
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1199 line 715
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound74 line 718