OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic132.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2112 line 15
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2112 line 18
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2112 line 20
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2112 line 22
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2113 line 26
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2113 line 29
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2113 line 31
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2113 line 33
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2114 line 37
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2114 line 40
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2114 line 42
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2114 line 44
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2115 line 48
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2115 line 51
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2115 line 53
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2115 line 55
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2116 line 59
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2116 line 62
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2116 line 64
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2116 line 66
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2117 line 70
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2117 line 73
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2117 line 75
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2117 line 77
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2118 line 81
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2118 line 84
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2118 line 86
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2118 line 88
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2119 line 92
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2119 line 95
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2119 line 97
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2119 line 99
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2120 line 103
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2120 line 106
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2120 line 108
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2120 line 110
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2121 line 114
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2121 line 117
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2121 line 119
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2121 line 121
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2122 line 125
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2122 line 128
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2122 line 130
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2122 line 132
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2123 line 136
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2123 line 139
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2123 line 141
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2123 line 143
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2124 line 147
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2124 line 150
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2124 line 152
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2124 line 154
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2125 line 158
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2125 line 161
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2125 line 163
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2125 line 165
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2126 line 169
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2126 line 172
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2126 line 174
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2126 line 176
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource2127 line 180
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow2127 line 183
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck2127 line 185
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck2127 line 187