OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical171.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5472 line 10
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5472 line 12
  3. def OAI.MUB6.Certificate.PairSemantics.raw5473 line 16
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5473 line 18
  5. def OAI.MUB6.Certificate.PairSemantics.raw5474 line 22
  6. def OAI.MUB6.Certificate.PairSemantics.raw5474step0 line 24
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical5474 line 26
  8. def OAI.MUB6.Certificate.PairSemantics.raw5475 line 35
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5475 line 37
  10. def OAI.MUB6.Certificate.PairSemantics.raw5476 line 41
  11. def OAI.MUB6.Certificate.PairSemantics.raw5476step0 line 43
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5476 line 45
  13. def OAI.MUB6.Certificate.PairSemantics.raw5477 line 54
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5477 line 56
  15. def OAI.MUB6.Certificate.PairSemantics.raw5478 line 60
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5478 line 62
  17. def OAI.MUB6.Certificate.PairSemantics.raw5479 line 66
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical5479 line 68
  19. def OAI.MUB6.Certificate.PairSemantics.raw5480 line 72
  20. def OAI.MUB6.Certificate.PairSemantics.raw5480step0 line 74
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5480 line 76
  22. def OAI.MUB6.Certificate.PairSemantics.raw5481 line 85
  23. def OAI.MUB6.Certificate.PairSemantics.raw5481step0 line 87
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5481 line 89
  25. def OAI.MUB6.Certificate.PairSemantics.raw5482 line 98
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5482 line 100
  27. def OAI.MUB6.Certificate.PairSemantics.raw5483 line 104
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5483 line 106
  29. def OAI.MUB6.Certificate.PairSemantics.raw5484 line 110
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5484 line 112
  31. def OAI.MUB6.Certificate.PairSemantics.raw5485 line 116
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5485 line 118
  33. def OAI.MUB6.Certificate.PairSemantics.raw5486 line 122
  34. def OAI.MUB6.Certificate.PairSemantics.raw5486step0 line 124
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5486 line 126
  36. def OAI.MUB6.Certificate.PairSemantics.raw5487 line 135
  37. def OAI.MUB6.Certificate.PairSemantics.raw5487step0 line 137
  38. def OAI.MUB6.Certificate.PairSemantics.raw5487step1 line 139
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5487 line 141
  40. def OAI.MUB6.Certificate.PairSemantics.raw5488 line 154
  41. def OAI.MUB6.Certificate.PairSemantics.raw5488step0 line 156
  42. def OAI.MUB6.Certificate.PairSemantics.raw5488step1 line 158
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5488 line 160
  44. def OAI.MUB6.Certificate.PairSemantics.raw5489 line 173
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical5489 line 175
  46. def OAI.MUB6.Certificate.PairSemantics.raw5490 line 179
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5490 line 181
  48. def OAI.MUB6.Certificate.PairSemantics.raw5491 line 185
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5491 line 187
  50. def OAI.MUB6.Certificate.PairSemantics.raw5492 line 191
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5492 line 193
  52. def OAI.MUB6.Certificate.PairSemantics.raw5493 line 197
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5493 line 199
  54. def OAI.MUB6.Certificate.PairSemantics.raw5494 line 203
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical5494 line 205
  56. def OAI.MUB6.Certificate.PairSemantics.raw5495 line 209
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical5495 line 211
  58. def OAI.MUB6.Certificate.PairSemantics.raw5496 line 215
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5496 line 217
  60. def OAI.MUB6.Certificate.PairSemantics.raw5497 line 221
  61. def OAI.MUB6.Certificate.PairSemantics.raw5497step0 line 223
  62. def OAI.MUB6.Certificate.PairSemantics.raw5497step1 line 225
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical5497 line 227
  64. def OAI.MUB6.Certificate.PairSemantics.raw5498 line 240
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5498 line 242
  66. def OAI.MUB6.Certificate.PairSemantics.raw5499 line 246
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5499 line 248
  68. def OAI.MUB6.Certificate.PairSemantics.raw5500 line 252
  69. def OAI.MUB6.Certificate.PairSemantics.raw5500step0 line 254
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical5500 line 256
  71. def OAI.MUB6.Certificate.PairSemantics.raw5501 line 265
  72. def OAI.MUB6.Certificate.PairSemantics.raw5501step0 line 267
  73. def OAI.MUB6.Certificate.PairSemantics.raw5501step1 line 269
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5501 line 271
  75. def OAI.MUB6.Certificate.PairSemantics.raw5502 line 284
  76. def OAI.MUB6.Certificate.PairSemantics.raw5502step0 line 286
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5502 line 288
  78. def OAI.MUB6.Certificate.PairSemantics.raw5503 line 298
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5503 line 300