OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical145.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4640 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw4640step0 line 23
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical4640 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw4641 line 34
  5. def OAI.MUB6.Certificate.PairSemantics.raw4641step0 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw4641step1 line 38
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4641 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw4642 line 53
  9. def OAI.MUB6.Certificate.PairSemantics.raw4642step0 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw4642step1 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4642 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw4643 line 72
  13. def OAI.MUB6.Certificate.PairSemantics.raw4643step0 line 74
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4643 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw4644 line 85
  16. def OAI.MUB6.Certificate.PairSemantics.raw4644step0 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw4644step1 line 89
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4644 line 91
  19. def OAI.MUB6.Certificate.PairSemantics.raw4645 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw4645step0 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw4645step1 line 108
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4645 line 110
  23. def OAI.MUB6.Certificate.PairSemantics.raw4646 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw4646step0 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4646 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw4647 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw4647step0 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw4647step1 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4647 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw4648 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw4648step0 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw4648step1 line 159
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4648 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw4649 line 174
  35. def OAI.MUB6.Certificate.PairSemantics.raw4649step0 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw4649step1 line 178
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4649 line 180
  38. def OAI.MUB6.Certificate.PairSemantics.raw4650 line 193
  39. def OAI.MUB6.Certificate.PairSemantics.raw4650step0 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw4650step1 line 197
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical4650 line 199
  42. def OAI.MUB6.Certificate.PairSemantics.raw4651 line 212
  43. def OAI.MUB6.Certificate.PairSemantics.raw4651step0 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw4651step1 line 216
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical4651 line 218
  46. def OAI.MUB6.Certificate.PairSemantics.raw4652 line 231
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4652 line 233
  48. def OAI.MUB6.Certificate.PairSemantics.raw4653 line 237
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical4653 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw4654 line 243
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4654 line 245
  52. def OAI.MUB6.Certificate.PairSemantics.raw4655 line 249
  53. def OAI.MUB6.Certificate.PairSemantics.raw4655step0 line 251
  54. def OAI.MUB6.Certificate.PairSemantics.raw4655step1 line 253
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4655 line 255
  56. def OAI.MUB6.Certificate.PairSemantics.raw4656 line 268
  57. def OAI.MUB6.Certificate.PairSemantics.raw4656step0 line 270
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4656 line 272
  59. def OAI.MUB6.Certificate.PairSemantics.raw4657 line 281
  60. def OAI.MUB6.Certificate.PairSemantics.raw4657step0 line 283
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4657 line 285
  62. def OAI.MUB6.Certificate.PairSemantics.raw4658 line 294
  63. def OAI.MUB6.Certificate.PairSemantics.raw4658step0 line 296
  64. def OAI.MUB6.Certificate.PairSemantics.raw4658step1 line 298
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4658 line 300
  66. def OAI.MUB6.Certificate.PairSemantics.raw4659 line 313
  67. def OAI.MUB6.Certificate.PairSemantics.raw4659step0 line 315
  68. def OAI.MUB6.Certificate.PairSemantics.raw4659step1 line 317
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4659 line 319
  70. def OAI.MUB6.Certificate.PairSemantics.raw4660 line 332
  71. def OAI.MUB6.Certificate.PairSemantics.raw4660step0 line 334
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4660 line 336
  73. def OAI.MUB6.Certificate.PairSemantics.raw4661 line 345
  74. def OAI.MUB6.Certificate.PairSemantics.raw4661step0 line 347
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4661 line 349
  76. def OAI.MUB6.Certificate.PairSemantics.raw4662 line 358
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4662 line 360
  78. def OAI.MUB6.Certificate.PairSemantics.raw4663 line 364
  79. def OAI.MUB6.Certificate.PairSemantics.raw4663step0 line 366
  80. def OAI.MUB6.Certificate.PairSemantics.raw4663step1 line 368
  81. def OAI.MUB6.Certificate.PairSemantics.raw4663step2 line 370
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4663 line 372
  83. def OAI.MUB6.Certificate.PairSemantics.raw4664 line 389
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4664 line 391
  85. def OAI.MUB6.Certificate.PairSemantics.raw4665 line 395
  86. def OAI.MUB6.Certificate.PairSemantics.raw4665step0 line 397
  87. def OAI.MUB6.Certificate.PairSemantics.raw4665step1 line 399
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4665 line 401
  89. def OAI.MUB6.Certificate.PairSemantics.raw4666 line 414
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4666 line 416
  91. def OAI.MUB6.Certificate.PairSemantics.raw4667 line 420
  92. def OAI.MUB6.Certificate.PairSemantics.raw4667step0 line 422
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4667 line 424
  94. def OAI.MUB6.Certificate.PairSemantics.raw4668 line 433
  95. def OAI.MUB6.Certificate.PairSemantics.raw4668step0 line 435
  96. def OAI.MUB6.Certificate.PairSemantics.raw4668step1 line 437
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical4668 line 439
  98. def OAI.MUB6.Certificate.PairSemantics.raw4669 line 452
  99. def OAI.MUB6.Certificate.PairSemantics.raw4669step0 line 454
  100. def OAI.MUB6.Certificate.PairSemantics.raw4669step1 line 456
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4669 line 458
  102. def OAI.MUB6.Certificate.PairSemantics.raw4670 line 471
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical4670 line 473
  104. def OAI.MUB6.Certificate.PairSemantics.raw4671 line 477
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical4671 line 479