OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic126.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2016 line 50
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2016 line 53
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2016 line 55
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2016 line 57
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2017 line 62
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2017 line 65
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2017 line 67
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2017 line 69
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2018 line 73
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2018 line 76
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2018 line 78
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2018 line 80
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2019 line 85
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2019 line 88
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2019 line 90
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2019 line 92
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2020 line 97
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2020 line 100
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2020 line 102
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2020 line 104
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2021 line 108
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2021 line 111
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2021 line 113
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2021 line 115
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2022 line 120
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2022 line 123
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2022 line 125
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2022 line 127
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2023 line 132
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2023 line 135
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2023 line 137
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2023 line 139
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2024 line 144
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2024 line 147
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2024 line 149
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2024 line 151
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2025 line 155
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2025 line 158
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2025 line 160
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2025 line 162
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2026 line 166
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2026 line 169
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2026 line 171
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2026 line 173
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2027 line 177
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2027 line 180
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2027 line 182
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2027 line 184
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2028 line 188
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2028 line 191
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2028 line 193
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2028 line 195
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2029 line 199
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2029 line 202
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2029 line 204
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2029 line 206
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2030 line 210
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2030 line 213
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2030 line 215
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2030 line 217
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2031 line 221
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2031 line 224
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2031 line 226
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2031 line 228