OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic60.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource960 line 38
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow960 line 41
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck960 line 43
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck960 line 45
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource961 line 50
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow961 line 53
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck961 line 55
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck961 line 57
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource962 line 62
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow962 line 65
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck962 line 67
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck962 line 69
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource963 line 74
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow963 line 77
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck963 line 79
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck963 line 81
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource964 line 86
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow964 line 89
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck964 line 91
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck964 line 93
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource965 line 98
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow965 line 101
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck965 line 103
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck965 line 105
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource966 line 110
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow966 line 113
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck966 line 115
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck966 line 117
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource967 line 122
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow967 line 125
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck967 line 127
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck967 line 129
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource968 line 134
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow968 line 137
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck968 line 139
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck968 line 141
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource969 line 146
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow969 line 149
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck969 line 151
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck969 line 153
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource970 line 158
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow970 line 161
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck970 line 163
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck970 line 165
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource971 line 170
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow971 line 173
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck971 line 175
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck971 line 177
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource972 line 182
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow972 line 185
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck972 line 187
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck972 line 189
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource973 line 194
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow973 line 197
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck973 line 199
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck973 line 201
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource974 line 206
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow974 line 209
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck974 line 211
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck974 line 213
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource975 line 218
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow975 line 221
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck975 line 223
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck975 line 225