OAI/Analysis/MutuallyUnbiased/MixedSources/Rows84.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1344 line 29
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1344 line 56
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1345 line 61
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1345 line 88
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1346 line 93
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1346 line 120
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1347 line 125
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1347 line 152
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1348 line 157
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1348 line 184
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1349 line 189
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1349 line 216
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1350 line 221
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1350 line 245
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1351 line 250
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1351 line 274
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1352 line 279
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1352 line 303
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1353 line 308
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1353 line 332
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1354 line 337
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1354 line 364
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1355 line 369
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1355 line 396
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1356 line 401
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1356 line 428
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1357 line 433
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1357 line 457
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1358 line 462
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1358 line 486
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1359 line 491
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1359 line 512
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1344 line 517
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1345 line 520
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1346 line 523
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1347 line 526
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1348 line 529
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1349 line 532
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1350 line 535
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1351 line 538
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1352 line 541
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1353 line 544
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1354 line 547
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1355 line 550
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1356 line 553
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1357 line 556
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1358 line 559
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1359 line 562
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound84 line 565