OAI/Analysis/MutuallyUnbiased/MixedSources/Rows86.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1376 line 30
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1376 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1377 line 62
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1377 line 86
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1378 line 91
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1378 line 118
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1379 line 123
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1379 line 150
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1380 line 155
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1380 line 182
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1381 line 187
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1381 line 214
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1382 line 219
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1382 line 246
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1383 line 251
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1383 line 278
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1384 line 283
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1384 line 310
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1385 line 315
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1385 line 342
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1386 line 347
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1386 line 374
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1387 line 379
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1387 line 403
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1388 line 408
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1388 line 432
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1389 line 437
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1389 line 461
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1390 line 466
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1390 line 490
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1391 line 495
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1391 line 516
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1376 line 521
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1377 line 524
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1378 line 527
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1379 line 530
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1380 line 533
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1381 line 536
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1382 line 539
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1383 line 542
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1384 line 545
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1385 line 548
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1386 line 551
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1387 line 554
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1388 line 557
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1389 line 560
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1390 line 563
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1391 line 566
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound86 line 569