OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical23.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw736 line 15
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical736 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw737 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical737 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw738 line 27
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical738 line 29
  7. def OAI.MUB6.Certificate.PairSemantics.raw739 line 33
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical739 line 35
  9. def OAI.MUB6.Certificate.PairSemantics.raw740 line 39
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical740 line 41
  11. def OAI.MUB6.Certificate.PairSemantics.raw741 line 45
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical741 line 47
  13. def OAI.MUB6.Certificate.PairSemantics.raw742 line 51
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical742 line 53
  15. def OAI.MUB6.Certificate.PairSemantics.raw743 line 57
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical743 line 59
  17. def OAI.MUB6.Certificate.PairSemantics.raw744 line 63
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical744 line 65
  19. def OAI.MUB6.Certificate.PairSemantics.raw745 line 69
  20. def OAI.MUB6.Certificate.PairSemantics.raw745step0 line 71
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical745 line 73
  22. def OAI.MUB6.Certificate.PairSemantics.raw746 line 82
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical746 line 84
  24. def OAI.MUB6.Certificate.PairSemantics.raw747 line 88
  25. def OAI.MUB6.Certificate.PairSemantics.raw747step0 line 90
  26. def OAI.MUB6.Certificate.PairSemantics.raw747step1 line 92
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical747 line 94
  28. def OAI.MUB6.Certificate.PairSemantics.raw748 line 107
  29. def OAI.MUB6.Certificate.PairSemantics.raw748step0 line 109
  30. def OAI.MUB6.Certificate.PairSemantics.raw748step1 line 111
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical748 line 113
  32. def OAI.MUB6.Certificate.PairSemantics.raw749 line 126
  33. def OAI.MUB6.Certificate.PairSemantics.raw749step0 line 128
  34. def OAI.MUB6.Certificate.PairSemantics.raw749step1 line 130
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical749 line 132
  36. def OAI.MUB6.Certificate.PairSemantics.raw750 line 145
  37. def OAI.MUB6.Certificate.PairSemantics.raw750step0 line 147
  38. def OAI.MUB6.Certificate.PairSemantics.raw750step1 line 149
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical750 line 151
  40. def OAI.MUB6.Certificate.PairSemantics.raw751 line 164
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical751 line 166
  42. def OAI.MUB6.Certificate.PairSemantics.raw752 line 170
  43. def OAI.MUB6.Certificate.PairSemantics.raw752step0 line 172
  44. def OAI.MUB6.Certificate.PairSemantics.raw752step1 line 174
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical752 line 176
  46. def OAI.MUB6.Certificate.PairSemantics.raw753 line 190
  47. def OAI.MUB6.Certificate.PairSemantics.raw753step0 line 192
  48. def OAI.MUB6.Certificate.PairSemantics.raw753step1 line 194
  49. def OAI.MUB6.Certificate.PairSemantics.raw753step2 line 196
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical753 line 198
  51. def OAI.MUB6.Certificate.PairSemantics.raw754 line 216
  52. def OAI.MUB6.Certificate.PairSemantics.raw754step0 line 218
  53. def OAI.MUB6.Certificate.PairSemantics.raw754step1 line 220
  54. def OAI.MUB6.Certificate.PairSemantics.raw754step2 line 222
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical754 line 224
  56. def OAI.MUB6.Certificate.PairSemantics.raw755 line 242
  57. def OAI.MUB6.Certificate.PairSemantics.raw755step0 line 244
  58. def OAI.MUB6.Certificate.PairSemantics.raw755step1 line 246
  59. def OAI.MUB6.Certificate.PairSemantics.raw755step2 line 248
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical755 line 250
  61. def OAI.MUB6.Certificate.PairSemantics.raw756 line 268
  62. def OAI.MUB6.Certificate.PairSemantics.raw756step0 line 270
  63. def OAI.MUB6.Certificate.PairSemantics.raw756step1 line 272
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical756 line 274
  65. def OAI.MUB6.Certificate.PairSemantics.raw757 line 288
  66. def OAI.MUB6.Certificate.PairSemantics.raw757step0 line 290
  67. def OAI.MUB6.Certificate.PairSemantics.raw757step1 line 292
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical757 line 294
  69. def OAI.MUB6.Certificate.PairSemantics.raw758 line 308
  70. def OAI.MUB6.Certificate.PairSemantics.raw758step0 line 310
  71. def OAI.MUB6.Certificate.PairSemantics.raw758step1 line 312
  72. def OAI.MUB6.Certificate.PairSemantics.raw758step2 line 314
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical758 line 316
  74. def OAI.MUB6.Certificate.PairSemantics.raw759 line 334
  75. def OAI.MUB6.Certificate.PairSemantics.raw759step0 line 336
  76. def OAI.MUB6.Certificate.PairSemantics.raw759step1 line 338
  77. def OAI.MUB6.Certificate.PairSemantics.raw759step2 line 340
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical759 line 342
  79. def OAI.MUB6.Certificate.PairSemantics.raw760 line 360
  80. def OAI.MUB6.Certificate.PairSemantics.raw760step0 line 362
  81. def OAI.MUB6.Certificate.PairSemantics.raw760step1 line 364
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical760 line 366
  83. def OAI.MUB6.Certificate.PairSemantics.raw761 line 380
  84. def OAI.MUB6.Certificate.PairSemantics.raw761step0 line 382
  85. def OAI.MUB6.Certificate.PairSemantics.raw761step1 line 384
  86. def OAI.MUB6.Certificate.PairSemantics.raw761step2 line 386
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical761 line 388
  88. def OAI.MUB6.Certificate.PairSemantics.raw762 line 406
  89. def OAI.MUB6.Certificate.PairSemantics.raw762step0 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw762step1 line 410
  91. def OAI.MUB6.Certificate.PairSemantics.raw762step2 line 412
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical762 line 414
  93. def OAI.MUB6.Certificate.PairSemantics.raw763 line 432
  94. def OAI.MUB6.Certificate.PairSemantics.raw763step0 line 434
  95. def OAI.MUB6.Certificate.PairSemantics.raw763step1 line 436
  96. def OAI.MUB6.Certificate.PairSemantics.raw763step2 line 438
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical763 line 440
  98. def OAI.MUB6.Certificate.PairSemantics.raw764 line 458
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical764 line 460
  100. def OAI.MUB6.Certificate.PairSemantics.raw765 line 464
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical765 line 466
  102. def OAI.MUB6.Certificate.PairSemantics.raw766 line 470
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical766 line 472
  104. def OAI.MUB6.Certificate.PairSemantics.raw767 line 476
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical767 line 478