OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic42.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource672 line 43
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow672 line 46
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck672 line 48
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck672 line 50
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource673 line 54
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow673 line 57
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck673 line 59
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck673 line 61
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource674 line 65
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow674 line 68
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck674 line 70
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck674 line 72
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource675 line 76
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow675 line 79
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck675 line 81
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck675 line 83
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource676 line 88
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow676 line 91
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck676 line 93
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck676 line 95
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource677 line 99
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow677 line 102
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck677 line 104
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck677 line 106
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource678 line 110
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow678 line 113
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck678 line 115
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck678 line 117
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource679 line 121
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow679 line 124
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck679 line 126
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck679 line 128
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource680 line 132
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow680 line 135
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck680 line 137
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck680 line 139
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource681 line 143
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow681 line 146
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck681 line 148
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck681 line 150
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource682 line 154
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow682 line 157
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck682 line 159
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck682 line 161
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource683 line 166
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow683 line 169
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck683 line 171
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck683 line 173
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource684 line 178
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow684 line 181
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck684 line 183
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck684 line 185
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource685 line 189
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow685 line 192
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck685 line 194
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck685 line 196
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource686 line 200
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow686 line 203
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck686 line 205
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck686 line 207
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource687 line 212
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow687 line 215
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck687 line 217
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck687 line 219