OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic32.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource512 line 56
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow512 line 59
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck512 line 61
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck512 line 63
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource513 line 68
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow513 line 71
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck513 line 73
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck513 line 75
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource514 line 80
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow514 line 83
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck514 line 85
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck514 line 87
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource515 line 92
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow515 line 95
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck515 line 97
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck515 line 99
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource516 line 104
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow516 line 107
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck516 line 109
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck516 line 111
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource517 line 116
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow517 line 119
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck517 line 121
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck517 line 123
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource518 line 127
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow518 line 130
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck518 line 132
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck518 line 134
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource519 line 139
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow519 line 142
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck519 line 144
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck519 line 146
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource520 line 151
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow520 line 154
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck520 line 156
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck520 line 158
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource521 line 163
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow521 line 166
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck521 line 168
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck521 line 170
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource522 line 175
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow522 line 178
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck522 line 180
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck522 line 182
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource523 line 187
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow523 line 190
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck523 line 192
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck523 line 194
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource524 line 199
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow524 line 202
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck524 line 204
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck524 line 206
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource525 line 211
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow525 line 214
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck525 line 216
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck525 line 218
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource526 line 223
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow526 line 226
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck526 line 228
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck526 line 230
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource527 line 235
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow527 line 238
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck527 line 240
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck527 line 242