OAI/Analysis/MutuallyUnbiased/MixedSources/Arithmetic41.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource656 line 54
  2. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow656 line 57
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck656 line 59
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck656 line 61
  5. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource657 line 66
  6. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow657 line 69
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck657 line 71
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck657 line 73
  9. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource658 line 78
  10. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow658 line 81
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck658 line 83
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck658 line 85
  13. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource659 line 90
  14. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow659 line 93
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck659 line 95
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck659 line 97
  17. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource660 line 102
  18. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow660 line 105
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck660 line 107
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck660 line 109
  21. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource661 line 114
  22. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow661 line 117
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck661 line 119
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck661 line 121
  25. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource662 line 125
  26. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow662 line 128
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck662 line 130
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck662 line 132
  29. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource663 line 136
  30. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow663 line 139
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck663 line 141
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck663 line 143
  33. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource664 line 148
  34. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow664 line 151
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck664 line 153
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck664 line 155
  37. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource665 line 160
  38. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow665 line 163
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck665 line 165
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck665 line 167
  41. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource666 line 171
  42. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow666 line 174
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck666 line 176
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck666 line 178
  45. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource667 line 183
  46. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow667 line 186
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck667 line 188
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck667 line 190
  49. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource668 line 195
  50. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow668 line 198
  51. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck668 line 200
  52. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck668 line 202
  53. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource669 line 207
  54. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow669 line 210
  55. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck669 line 212
  56. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck669 line 214
  57. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource670 line 218
  58. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow670 line 221
  59. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck670 line 223
  60. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck670 line 225
  61. def OAI.MUB6.Certificate.MixedSourceBridge.reducedSource671 line 229
  62. def OAI.MUB6.Certificate.MixedSourceBridge.numericRow671 line 232
  63. theorem OAI.MUB6.Certificate.MixedSourceBridge.reindexCheck671 line 234
  64. theorem OAI.MUB6.Certificate.MixedSourceBridge.numericCheck671 line 236