OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical272.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8704 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw8704step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw8704step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8704 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw8705 line 41
  6. def OAI.MUB6.Certificate.PairSemantics.raw8705step0 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw8705step1 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8705 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw8706 line 61
  10. def OAI.MUB6.Certificate.PairSemantics.raw8706step0 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw8706step1 line 65
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8706 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw8707 line 81
  14. def OAI.MUB6.Certificate.PairSemantics.raw8707step0 line 83
  15. def OAI.MUB6.Certificate.PairSemantics.raw8707step1 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw8707step2 line 87
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical8707 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw8708 line 107
  19. def OAI.MUB6.Certificate.PairSemantics.raw8708step0 line 109
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8708 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw8709 line 120
  22. def OAI.MUB6.Certificate.PairSemantics.raw8709step0 line 122
  23. def OAI.MUB6.Certificate.PairSemantics.raw8709step1 line 124
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8709 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw8710 line 139
  26. def OAI.MUB6.Certificate.PairSemantics.raw8710step0 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw8710step1 line 143
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8710 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw8711 line 158
  30. def OAI.MUB6.Certificate.PairSemantics.raw8711step0 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw8711step1 line 162
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical8711 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw8712 line 178
  34. def OAI.MUB6.Certificate.PairSemantics.raw8712step0 line 180
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8712 line 182
  36. def OAI.MUB6.Certificate.PairSemantics.raw8713 line 191
  37. def OAI.MUB6.Certificate.PairSemantics.raw8713step0 line 193
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8713 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw8714 line 204
  40. def OAI.MUB6.Certificate.PairSemantics.raw8714step0 line 206
  41. def OAI.MUB6.Certificate.PairSemantics.raw8714step1 line 208
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical8714 line 210
  43. def OAI.MUB6.Certificate.PairSemantics.raw8715 line 224
  44. def OAI.MUB6.Certificate.PairSemantics.raw8715step0 line 226
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8715 line 228
  46. def OAI.MUB6.Certificate.PairSemantics.raw8716 line 237
  47. def OAI.MUB6.Certificate.PairSemantics.raw8716step0 line 239
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8716 line 241
  49. def OAI.MUB6.Certificate.PairSemantics.raw8717 line 250
  50. def OAI.MUB6.Certificate.PairSemantics.raw8717step0 line 252
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8717 line 254
  52. def OAI.MUB6.Certificate.PairSemantics.raw8718 line 263
  53. def OAI.MUB6.Certificate.PairSemantics.raw8718step0 line 265
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical8718 line 267
  55. def OAI.MUB6.Certificate.PairSemantics.raw8719 line 276
  56. def OAI.MUB6.Certificate.PairSemantics.raw8719step0 line 278
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8719 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw8720 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw8720step0 line 291
  60. def OAI.MUB6.Certificate.PairSemantics.raw8720step1 line 293
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8720 line 295
  62. def OAI.MUB6.Certificate.PairSemantics.raw8721 line 308
  63. def OAI.MUB6.Certificate.PairSemantics.raw8721step0 line 310
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8721 line 312
  65. def OAI.MUB6.Certificate.PairSemantics.raw8722 line 321
  66. def OAI.MUB6.Certificate.PairSemantics.raw8722step0 line 323
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical8722 line 325
  68. def OAI.MUB6.Certificate.PairSemantics.raw8723 line 334
  69. def OAI.MUB6.Certificate.PairSemantics.raw8723step0 line 336
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8723 line 338
  71. def OAI.MUB6.Certificate.PairSemantics.raw8724 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw8724step0 line 349
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8724 line 351
  74. def OAI.MUB6.Certificate.PairSemantics.raw8725 line 360
  75. def OAI.MUB6.Certificate.PairSemantics.raw8725step0 line 362
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8725 line 364
  77. def OAI.MUB6.Certificate.PairSemantics.raw8726 line 373
  78. def OAI.MUB6.Certificate.PairSemantics.raw8726step0 line 375
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8726 line 377
  80. def OAI.MUB6.Certificate.PairSemantics.raw8727 line 386
  81. def OAI.MUB6.Certificate.PairSemantics.raw8727step0 line 388
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8727 line 390
  83. def OAI.MUB6.Certificate.PairSemantics.raw8728 line 399
  84. def OAI.MUB6.Certificate.PairSemantics.raw8728step0 line 401
  85. def OAI.MUB6.Certificate.PairSemantics.raw8728step1 line 403
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8728 line 405
  87. def OAI.MUB6.Certificate.PairSemantics.raw8729 line 418
  88. def OAI.MUB6.Certificate.PairSemantics.raw8729step0 line 420
  89. def OAI.MUB6.Certificate.PairSemantics.raw8729step1 line 422
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical8729 line 424
  91. def OAI.MUB6.Certificate.PairSemantics.raw8730 line 438
  92. def OAI.MUB6.Certificate.PairSemantics.raw8730step0 line 440
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8730 line 442
  94. def OAI.MUB6.Certificate.PairSemantics.raw8731 line 451
  95. def OAI.MUB6.Certificate.PairSemantics.raw8731step0 line 453
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8731 line 455
  97. def OAI.MUB6.Certificate.PairSemantics.raw8732 line 464
  98. def OAI.MUB6.Certificate.PairSemantics.raw8732step0 line 466
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8732 line 468
  100. def OAI.MUB6.Certificate.PairSemantics.raw8733 line 477
  101. def OAI.MUB6.Certificate.PairSemantics.raw8733step0 line 479
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8733 line 481
  103. def OAI.MUB6.Certificate.PairSemantics.raw8734 line 490
  104. def OAI.MUB6.Certificate.PairSemantics.raw8734step0 line 492
  105. def OAI.MUB6.Certificate.PairSemantics.raw8734step1 line 494
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical8734 line 496
  107. def OAI.MUB6.Certificate.PairSemantics.raw8735 line 509
  108. def OAI.MUB6.Certificate.PairSemantics.raw8735step0 line 511
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical8735 line 513