OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic30.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource480 line 50
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow480 line 53
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck480 line 55
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck480 line 57
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource481 line 61
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow481 line 64
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck481 line 66
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck481 line 68
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource482 line 73
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow482 line 76
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck482 line 78
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck482 line 80
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource483 line 85
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow483 line 88
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck483 line 90
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck483 line 92
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource484 line 97
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow484 line 100
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck484 line 102
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck484 line 104
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource485 line 109
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow485 line 112
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck485 line 114
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck485 line 116
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource486 line 121
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow486 line 124
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck486 line 126
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck486 line 128
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource487 line 132
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow487 line 135
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck487 line 137
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck487 line 139
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource488 line 144
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow488 line 147
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck488 line 149
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck488 line 151
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource489 line 156
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow489 line 159
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck489 line 161
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck489 line 163
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource490 line 168
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow490 line 171
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck490 line 173
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck490 line 175
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource491 line 179
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow491 line 182
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck491 line 184
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck491 line 186
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource492 line 190
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow492 line 193
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck492 line 195
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck492 line 197
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource493 line 201
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow493 line 204
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck493 line 206
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck493 line 208
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource494 line 212
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow494 line 215
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck494 line 217
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck494 line 219
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource495 line 223
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow495 line 226
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck495 line 228
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck495 line 230