OAI/Analysis/MutuallyUnbiased/MixedSources/Rows85.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1360 line 32
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1360 line 53
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1361 line 58
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1361 line 82
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1362 line 87
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1362 line 108
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1363 line 113
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1363 line 137
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1364 line 142
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1364 line 169
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1365 line 174
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1365 line 198
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1366 line 203
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1366 line 224
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1367 line 229
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1367 line 253
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1368 line 258
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1368 line 279
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1369 line 284
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1369 line 308
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1370 line 313
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1370 line 334
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1371 line 339
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1371 line 366
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1372 line 371
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1372 line 395
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1373 line 400
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1373 line 427
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1374 line 432
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1374 line 456
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1375 line 461
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1375 line 488
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1360 line 493
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1361 line 496
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1362 line 499
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1363 line 502
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1364 line 505
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1365 line 508
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1366 line 511
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1367 line 514
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1368 line 517
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1369 line 520
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1370 line 523
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1371 line 526
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1372 line 529
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1373 line 532
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1374 line 535
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1375 line 538
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound85 line 541