OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic87.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1392 line 29
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1392 line 32
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1392 line 34
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1392 line 36
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1393 line 40
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1393 line 43
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1393 line 45
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1393 line 47
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1394 line 51
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1394 line 54
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1394 line 56
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1394 line 58
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1395 line 62
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1395 line 65
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1395 line 67
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1395 line 69
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1396 line 73
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1396 line 76
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1396 line 78
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1396 line 80
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1397 line 84
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1397 line 87
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1397 line 89
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1397 line 91
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1398 line 95
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1398 line 98
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1398 line 100
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1398 line 102
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1399 line 106
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1399 line 109
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1399 line 111
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1399 line 113
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1400 line 117
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1400 line 120
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1400 line 122
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1400 line 124
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1401 line 128
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1401 line 131
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1401 line 133
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1401 line 135
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1402 line 139
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1402 line 142
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1402 line 144
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1402 line 146
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1403 line 150
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1403 line 153
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1403 line 155
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1403 line 157
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1404 line 161
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1404 line 164
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1404 line 166
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1404 line 168
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1405 line 172
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1405 line 175
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1405 line 177
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1405 line 179
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1406 line 183
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1406 line 186
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1406 line 188
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1406 line 190
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1407 line 194
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1407 line 197
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1407 line 199
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1407 line 201