OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic34.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource544 line 45
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow544 line 48
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck544 line 50
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck544 line 52
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource545 line 56
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow545 line 59
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck545 line 61
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck545 line 63
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource546 line 68
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow546 line 71
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck546 line 73
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck546 line 75
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource547 line 80
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow547 line 83
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck547 line 85
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck547 line 87
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource548 line 92
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow548 line 95
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck548 line 97
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck548 line 99
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource549 line 104
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow549 line 107
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck549 line 109
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck549 line 111
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource550 line 115
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow550 line 118
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck550 line 120
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck550 line 122
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource551 line 126
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow551 line 129
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck551 line 131
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck551 line 133
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource552 line 138
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow552 line 141
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck552 line 143
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck552 line 145
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource553 line 150
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow553 line 153
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck553 line 155
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck553 line 157
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource554 line 162
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow554 line 165
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck554 line 167
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck554 line 169
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource555 line 174
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow555 line 177
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck555 line 179
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck555 line 181
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource556 line 186
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow556 line 189
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck556 line 191
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck556 line 193
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource557 line 197
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow557 line 200
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck557 line 202
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck557 line 204
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource558 line 209
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow558 line 212
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck558 line 214
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck558 line 216
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource559 line 221
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow559 line 224
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck559 line 226
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck559 line 228