OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical148.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4736 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4736step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw4736step1 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw4736step2 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4736 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw4737 line 45
  7. def OAI.MUB6.Certificate.PairSemantics.raw4737step0 line 47
  8. def OAI.MUB6.Certificate.PairSemantics.raw4737step1 line 49
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4737 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw4738 line 64
  11. def OAI.MUB6.Certificate.PairSemantics.raw4738step0 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw4738step1 line 68
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4738 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw4739 line 83
  15. def OAI.MUB6.Certificate.PairSemantics.raw4739step0 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw4739step1 line 87
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4739 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw4740 line 102
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4740 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw4741 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw4741step0 line 110
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4741 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw4742 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw4742step0 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw4742step1 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw4742step2 line 127
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4742 line 129
  28. def OAI.MUB6.Certificate.PairSemantics.raw4743 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw4743step0 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw4743step1 line 150
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4743 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw4744 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw4744step0 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw4744step1 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw4744step2 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4744 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw4745 line 190
  38. def OAI.MUB6.Certificate.PairSemantics.raw4745step0 line 192
  39. def OAI.MUB6.Certificate.PairSemantics.raw4745step1 line 194
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4745 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw4746 line 209
  42. def OAI.MUB6.Certificate.PairSemantics.raw4746step0 line 211
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4746 line 213
  44. def OAI.MUB6.Certificate.PairSemantics.raw4747 line 222
  45. def OAI.MUB6.Certificate.PairSemantics.raw4747step0 line 224
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4747 line 226
  47. def OAI.MUB6.Certificate.PairSemantics.raw4748 line 235
  48. def OAI.MUB6.Certificate.PairSemantics.raw4748step0 line 237
  49. def OAI.MUB6.Certificate.PairSemantics.raw4748step1 line 239
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4748 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw4749 line 254
  52. def OAI.MUB6.Certificate.PairSemantics.raw4749step0 line 256
  53. def OAI.MUB6.Certificate.PairSemantics.raw4749step1 line 258
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4749 line 260
  55. def OAI.MUB6.Certificate.PairSemantics.raw4750 line 273
  56. def OAI.MUB6.Certificate.PairSemantics.raw4750step0 line 275
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4750 line 277
  58. def OAI.MUB6.Certificate.PairSemantics.raw4751 line 286
  59. def OAI.MUB6.Certificate.PairSemantics.raw4751step0 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw4751step1 line 290
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4751 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw4752 line 305
  63. def OAI.MUB6.Certificate.PairSemantics.raw4752step0 line 307
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4752 line 309
  65. def OAI.MUB6.Certificate.PairSemantics.raw4753 line 318
  66. def OAI.MUB6.Certificate.PairSemantics.raw4753step0 line 320
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4753 line 322
  68. def OAI.MUB6.Certificate.PairSemantics.raw4754 line 331
  69. def OAI.MUB6.Certificate.PairSemantics.raw4754step0 line 333
  70. def OAI.MUB6.Certificate.PairSemantics.raw4754step1 line 335
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4754 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw4755 line 350
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4755 line 352
  74. def OAI.MUB6.Certificate.PairSemantics.raw4756 line 356
  75. def OAI.MUB6.Certificate.PairSemantics.raw4756step0 line 358
  76. def OAI.MUB6.Certificate.PairSemantics.raw4756step1 line 360
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4756 line 362
  78. def OAI.MUB6.Certificate.PairSemantics.raw4757 line 375
  79. def OAI.MUB6.Certificate.PairSemantics.raw4757step0 line 377
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4757 line 379
  81. def OAI.MUB6.Certificate.PairSemantics.raw4758 line 388
  82. def OAI.MUB6.Certificate.PairSemantics.raw4758step0 line 390
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4758 line 392
  84. def OAI.MUB6.Certificate.PairSemantics.raw4759 line 401
  85. def OAI.MUB6.Certificate.PairSemantics.raw4759step0 line 403
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4759 line 405
  87. def OAI.MUB6.Certificate.PairSemantics.raw4760 line 414
  88. def OAI.MUB6.Certificate.PairSemantics.raw4760step0 line 416
  89. def OAI.MUB6.Certificate.PairSemantics.raw4760step1 line 418
  90. def OAI.MUB6.Certificate.PairSemantics.raw4760step2 line 420
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical4760 line 422
  92. def OAI.MUB6.Certificate.PairSemantics.raw4761 line 440
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4761 line 442
  94. def OAI.MUB6.Certificate.PairSemantics.raw4762 line 446
  95. def OAI.MUB6.Certificate.PairSemantics.raw4762step0 line 448
  96. def OAI.MUB6.Certificate.PairSemantics.raw4762step1 line 450
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4762 line 452
  98. def OAI.MUB6.Certificate.PairSemantics.raw4763 line 465
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical4763 line 467
  100. def OAI.MUB6.Certificate.PairSemantics.raw4764 line 471
  101. def OAI.MUB6.Certificate.PairSemantics.raw4764step0 line 473
  102. def OAI.MUB6.Certificate.PairSemantics.raw4764step1 line 475
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4764 line 477
  104. def OAI.MUB6.Certificate.PairSemantics.raw4765 line 490
  105. def OAI.MUB6.Certificate.PairSemantics.raw4765step0 line 492
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical4765 line 494
  107. def OAI.MUB6.Certificate.PairSemantics.raw4766 line 503
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4766 line 505
  109. def OAI.MUB6.Certificate.PairSemantics.raw4767 line 509
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical4767 line 511