OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic20.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource320 line 43
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow320 line 46
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck320 line 48
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck320 line 50
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource321 line 54
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow321 line 57
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck321 line 59
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck321 line 61
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource322 line 65
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow322 line 68
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck322 line 70
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck322 line 72
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource323 line 76
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow323 line 79
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck323 line 81
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck323 line 83
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource324 line 87
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow324 line 90
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck324 line 92
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck324 line 94
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource325 line 98
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow325 line 101
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck325 line 103
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck325 line 105
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource326 line 109
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow326 line 112
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck326 line 114
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck326 line 116
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource327 line 121
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow327 line 124
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck327 line 126
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck327 line 128
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource328 line 133
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow328 line 136
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck328 line 138
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck328 line 140
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource329 line 145
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow329 line 148
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck329 line 150
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck329 line 152
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource330 line 156
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow330 line 159
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck330 line 161
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck330 line 163
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource331 line 167
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow331 line 170
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck331 line 172
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck331 line 174
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource332 line 178
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow332 line 181
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck332 line 183
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck332 line 185
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource333 line 189
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow333 line 192
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck333 line 194
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck333 line 196
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource334 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow334 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck334 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck334 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource335 line 211
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow335 line 214
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck335 line 216
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck335 line 218