OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic68.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1088 line 42
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1088 line 45
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1088 line 47
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1088 line 49
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1089 line 53
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1089 line 56
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1089 line 58
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1089 line 60
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1090 line 64
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1090 line 67
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1090 line 69
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1090 line 71
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1091 line 75
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1091 line 78
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1091 line 80
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1091 line 82
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1092 line 86
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1092 line 89
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1092 line 91
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1092 line 93
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1093 line 97
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1093 line 100
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1093 line 102
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1093 line 104
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1094 line 109
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1094 line 112
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1094 line 114
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1094 line 116
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1095 line 121
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1095 line 124
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1095 line 126
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1095 line 128
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1096 line 133
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1096 line 136
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1096 line 138
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1096 line 140
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1097 line 145
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1097 line 148
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1097 line 150
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1097 line 152
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1098 line 157
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1098 line 160
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1098 line 162
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1098 line 164
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1099 line 169
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1099 line 172
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1099 line 174
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1099 line 176
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1100 line 180
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1100 line 183
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1100 line 185
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1100 line 187
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1101 line 191
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1101 line 194
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1101 line 196
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1101 line 198
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1102 line 202
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1102 line 205
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1102 line 207
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1102 line 209
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource1103 line 214
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow1103 line 217
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck1103 line 219
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck1103 line 221