OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic36.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource576 line 50
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow576 line 53
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck576 line 55
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck576 line 57
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource577 line 61
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow577 line 64
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck577 line 66
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck577 line 68
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource578 line 72
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow578 line 75
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck578 line 77
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck578 line 79
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource579 line 83
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow579 line 86
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck579 line 88
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck579 line 90
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource580 line 94
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow580 line 97
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck580 line 99
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck580 line 101
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource581 line 105
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow581 line 108
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck581 line 110
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck581 line 112
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource582 line 116
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow582 line 119
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck582 line 121
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck582 line 123
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource583 line 127
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow583 line 130
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck583 line 132
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck583 line 134
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource584 line 138
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow584 line 141
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck584 line 143
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck584 line 145
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource585 line 149
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow585 line 152
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck585 line 154
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck585 line 156
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource586 line 160
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow586 line 163
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck586 line 165
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck586 line 167
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource587 line 171
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow587 line 174
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck587 line 176
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck587 line 178
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource588 line 182
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow588 line 185
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck588 line 187
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck588 line 189
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource589 line 193
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow589 line 196
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck589 line 198
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck589 line 200
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource590 line 204
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow590 line 207
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck590 line 209
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck590 line 211
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource591 line 215
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow591 line 218
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck591 line 220
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck591 line 222