OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic54.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource864 line 47
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow864 line 50
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck864 line 52
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck864 line 54
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource865 line 59
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow865 line 62
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck865 line 64
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck865 line 66
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource866 line 71
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow866 line 74
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck866 line 76
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck866 line 78
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource867 line 83
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow867 line 86
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck867 line 88
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck867 line 90
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource868 line 95
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow868 line 98
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck868 line 100
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck868 line 102
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource869 line 107
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow869 line 110
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck869 line 112
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck869 line 114
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource870 line 118
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow870 line 121
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck870 line 123
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck870 line 125
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource871 line 129
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow871 line 132
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck871 line 134
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck871 line 136
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource872 line 141
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow872 line 144
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck872 line 146
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck872 line 148
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource873 line 153
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow873 line 156
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck873 line 158
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck873 line 160
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource874 line 165
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow874 line 168
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck874 line 170
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck874 line 172
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource875 line 176
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow875 line 179
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck875 line 181
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck875 line 183
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource876 line 187
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow876 line 190
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck876 line 192
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck876 line 194
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource877 line 198
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow877 line 201
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck877 line 203
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck877 line 205
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource878 line 210
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow878 line 213
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck878 line 215
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck878 line 217
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource879 line 222
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow879 line 225
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck879 line 227
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck879 line 229