OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic90.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1440 line 39
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1440 line 42
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1440 line 44
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1440 line 46
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1441 line 50
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1441 line 53
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1441 line 55
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1441 line 57
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1442 line 62
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1442 line 65
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1442 line 67
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1442 line 69
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1443 line 74
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1443 line 77
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1443 line 79
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1443 line 81
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1444 line 85
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1444 line 88
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1444 line 90
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1444 line 92
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1445 line 96
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1445 line 99
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1445 line 101
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1445 line 103
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1446 line 107
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1446 line 110
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1446 line 112
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1446 line 114
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1447 line 118
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1447 line 121
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1447 line 123
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1447 line 125
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1448 line 129
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1448 line 132
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1448 line 134
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1448 line 136
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1449 line 140
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1449 line 143
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1449 line 145
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1449 line 147
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1450 line 151
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1450 line 154
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1450 line 156
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1450 line 158
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1451 line 162
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1451 line 165
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1451 line 167
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1451 line 169
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1452 line 173
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1452 line 176
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1452 line 178
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1452 line 180
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1453 line 184
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1453 line 187
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1453 line 189
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1453 line 191
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1454 line 195
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1454 line 198
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1454 line 200
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1454 line 202
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1455 line 206
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1455 line 209
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1455 line 211
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1455 line 213