OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical172.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5504 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw5504step0 line 12
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5504 line 14
  4. def OAI.MUB6.Certificate.PairSemantics.raw5505 line 23
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5505 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw5506 line 29
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical5506 line 31
  8. def OAI.MUB6.Certificate.PairSemantics.raw5507 line 35
  9. def OAI.MUB6.Certificate.PairSemantics.raw5507step0 line 37
  10. def OAI.MUB6.Certificate.PairSemantics.raw5507step1 line 39
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5507 line 41
  12. def OAI.MUB6.Certificate.PairSemantics.raw5508 line 54
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5508 line 56
  14. def OAI.MUB6.Certificate.PairSemantics.raw5509 line 60
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5509 line 62
  16. def OAI.MUB6.Certificate.PairSemantics.raw5510 line 66
  17. def OAI.MUB6.Certificate.PairSemantics.raw5510step0 line 68
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical5510 line 70
  19. def OAI.MUB6.Certificate.PairSemantics.raw5511 line 79
  20. def OAI.MUB6.Certificate.PairSemantics.raw5511step0 line 81
  21. def OAI.MUB6.Certificate.PairSemantics.raw5511step1 line 83
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5511 line 85
  23. def OAI.MUB6.Certificate.PairSemantics.raw5512 line 98
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5512 line 100
  25. def OAI.MUB6.Certificate.PairSemantics.raw5513 line 104
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5513 line 106
  27. def OAI.MUB6.Certificate.PairSemantics.raw5514 line 110
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5514 line 112
  29. def OAI.MUB6.Certificate.PairSemantics.raw5515 line 116
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5515 line 118
  31. def OAI.MUB6.Certificate.PairSemantics.raw5516 line 122
  32. def OAI.MUB6.Certificate.PairSemantics.raw5516step0 line 124
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5516 line 126
  34. def OAI.MUB6.Certificate.PairSemantics.raw5517 line 135
  35. def OAI.MUB6.Certificate.PairSemantics.raw5517step0 line 137
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical5517 line 139
  37. def OAI.MUB6.Certificate.PairSemantics.raw5518 line 149
  38. def OAI.MUB6.Certificate.PairSemantics.raw5518step0 line 151
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5518 line 153
  40. def OAI.MUB6.Certificate.PairSemantics.raw5519 line 163
  41. def OAI.MUB6.Certificate.PairSemantics.raw5519step0 line 165
  42. def OAI.MUB6.Certificate.PairSemantics.raw5519step1 line 167
  43. def OAI.MUB6.Certificate.PairSemantics.raw5519step2 line 169
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5519 line 171
  45. def OAI.MUB6.Certificate.PairSemantics.raw5520 line 189
  46. def OAI.MUB6.Certificate.PairSemantics.raw5520step0 line 191
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical5520 line 193
  48. def OAI.MUB6.Certificate.PairSemantics.raw5521 line 202
  49. def OAI.MUB6.Certificate.PairSemantics.raw5521step0 line 204
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical5521 line 206
  51. def OAI.MUB6.Certificate.PairSemantics.raw5522 line 215
  52. def OAI.MUB6.Certificate.PairSemantics.raw5522step0 line 217
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical5522 line 219
  54. def OAI.MUB6.Certificate.PairSemantics.raw5523 line 228
  55. def OAI.MUB6.Certificate.PairSemantics.raw5523step0 line 230
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5523 line 232
  57. def OAI.MUB6.Certificate.PairSemantics.raw5524 line 241
  58. def OAI.MUB6.Certificate.PairSemantics.raw5524step0 line 243
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5524 line 245
  60. def OAI.MUB6.Certificate.PairSemantics.raw5525 line 255
  61. def OAI.MUB6.Certificate.PairSemantics.raw5525step0 line 257
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5525 line 259
  63. def OAI.MUB6.Certificate.PairSemantics.raw5526 line 269
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5526 line 271
  65. def OAI.MUB6.Certificate.PairSemantics.raw5527 line 275
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5527 line 277
  67. def OAI.MUB6.Certificate.PairSemantics.raw5528 line 281
  68. def OAI.MUB6.Certificate.PairSemantics.raw5528step0 line 283
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5528 line 285
  70. def OAI.MUB6.Certificate.PairSemantics.raw5529 line 294
  71. def OAI.MUB6.Certificate.PairSemantics.raw5529step0 line 296
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5529 line 298
  73. def OAI.MUB6.Certificate.PairSemantics.raw5530 line 307
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5530 line 309
  75. def OAI.MUB6.Certificate.PairSemantics.raw5531 line 313
  76. def OAI.MUB6.Certificate.PairSemantics.raw5531step0 line 315
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5531 line 317
  78. def OAI.MUB6.Certificate.PairSemantics.raw5532 line 327
  79. def OAI.MUB6.Certificate.PairSemantics.raw5532step0 line 329
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5532 line 331
  81. def OAI.MUB6.Certificate.PairSemantics.raw5533 line 340
  82. def OAI.MUB6.Certificate.PairSemantics.raw5533step0 line 342
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical5533 line 344
  84. def OAI.MUB6.Certificate.PairSemantics.raw5534 line 353
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5534 line 355
  86. def OAI.MUB6.Certificate.PairSemantics.raw5535 line 359
  87. def OAI.MUB6.Certificate.PairSemantics.raw5535step0 line 361
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5535 line 363