OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical114.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3648 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw3648step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical3648 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw3649 line 30
  5. def OAI.MUB6.Certificate.PairSemantics.raw3649step0 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw3649step1 line 34
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3649 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw3650 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw3650step0 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw3650step1 line 53
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3650 line 55
  12. def OAI.MUB6.Certificate.PairSemantics.raw3651 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw3651step0 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3651 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw3652 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw3652step0 line 83
  17. def OAI.MUB6.Certificate.PairSemantics.raw3652step1 line 85
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3652 line 87
  19. def OAI.MUB6.Certificate.PairSemantics.raw3653 line 100
  20. def OAI.MUB6.Certificate.PairSemantics.raw3653step0 line 102
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3653 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw3654 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw3654step0 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3654 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw3655 line 126
  26. def OAI.MUB6.Certificate.PairSemantics.raw3655step0 line 128
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3655 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw3656 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw3656step0 line 141
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3656 line 143
  31. def OAI.MUB6.Certificate.PairSemantics.raw3657 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw3657step0 line 154
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3657 line 156
  34. def OAI.MUB6.Certificate.PairSemantics.raw3658 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw3658step0 line 167
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3658 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw3659 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3659step0 line 180
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3659 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw3660 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw3660step0 line 193
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3660 line 195
  43. def OAI.MUB6.Certificate.PairSemantics.raw3661 line 204
  44. def OAI.MUB6.Certificate.PairSemantics.raw3661step0 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw3661step1 line 208
  46. def OAI.MUB6.Certificate.PairSemantics.raw3661step2 line 210
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3661 line 212
  48. def OAI.MUB6.Certificate.PairSemantics.raw3662 line 229
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3662 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw3663 line 235
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3663 line 237
  52. def OAI.MUB6.Certificate.PairSemantics.raw3664 line 241
  53. def OAI.MUB6.Certificate.PairSemantics.raw3664step0 line 243
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical3664 line 245
  55. def OAI.MUB6.Certificate.PairSemantics.raw3665 line 254
  56. def OAI.MUB6.Certificate.PairSemantics.raw3665step0 line 256
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3665 line 258
  58. def OAI.MUB6.Certificate.PairSemantics.raw3666 line 267
  59. def OAI.MUB6.Certificate.PairSemantics.raw3666step0 line 269
  60. def OAI.MUB6.Certificate.PairSemantics.raw3666step1 line 271
  61. def OAI.MUB6.Certificate.PairSemantics.raw3666step2 line 273
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3666 line 275
  63. def OAI.MUB6.Certificate.PairSemantics.raw3667 line 292
  64. def OAI.MUB6.Certificate.PairSemantics.raw3667step0 line 294
  65. def OAI.MUB6.Certificate.PairSemantics.raw3667step1 line 296
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3667 line 298
  67. def OAI.MUB6.Certificate.PairSemantics.raw3668 line 311
  68. def OAI.MUB6.Certificate.PairSemantics.raw3668step0 line 313
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3668 line 315
  70. def OAI.MUB6.Certificate.PairSemantics.raw3669 line 324
  71. def OAI.MUB6.Certificate.PairSemantics.raw3669step0 line 326
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3669 line 328
  73. def OAI.MUB6.Certificate.PairSemantics.raw3670 line 337
  74. def OAI.MUB6.Certificate.PairSemantics.raw3670step0 line 339
  75. def OAI.MUB6.Certificate.PairSemantics.raw3670step1 line 341
  76. def OAI.MUB6.Certificate.PairSemantics.raw3670step2 line 343
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3670 line 345
  78. def OAI.MUB6.Certificate.PairSemantics.raw3671 line 362
  79. def OAI.MUB6.Certificate.PairSemantics.raw3671step0 line 364
  80. def OAI.MUB6.Certificate.PairSemantics.raw3671step1 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw3671step2 line 368
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3671 line 370
  83. def OAI.MUB6.Certificate.PairSemantics.raw3672 line 387
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3672 line 389
  85. def OAI.MUB6.Certificate.PairSemantics.raw3673 line 393
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical3673 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw3674 line 399
  88. def OAI.MUB6.Certificate.PairSemantics.raw3674step0 line 401
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3674 line 403
  90. def OAI.MUB6.Certificate.PairSemantics.raw3675 line 412
  91. def OAI.MUB6.Certificate.PairSemantics.raw3675step0 line 414
  92. def OAI.MUB6.Certificate.PairSemantics.raw3675step1 line 416
  93. def OAI.MUB6.Certificate.PairSemantics.raw3675step2 line 418
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3675 line 420
  95. def OAI.MUB6.Certificate.PairSemantics.raw3676 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw3676step0 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw3676step1 line 441
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3676 line 443
  99. def OAI.MUB6.Certificate.PairSemantics.raw3677 line 456
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3677 line 458
  101. def OAI.MUB6.Certificate.PairSemantics.raw3678 line 462
  102. def OAI.MUB6.Certificate.PairSemantics.raw3678step0 line 464
  103. def OAI.MUB6.Certificate.PairSemantics.raw3678step1 line 466
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3678 line 468
  105. def OAI.MUB6.Certificate.PairSemantics.raw3679 line 481
  106. def OAI.MUB6.Certificate.PairSemantics.raw3679step0 line 483
  107. def OAI.MUB6.Certificate.PairSemantics.raw3679step1 line 485
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical3679 line 487