OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical176.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5632 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw5632step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw5632step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical5632 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw5633 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw5633step0 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw5633step1 line 40
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5633 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw5634 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw5634step0 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw5634step1 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical5634 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw5635 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw5635step0 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw5635step1 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5635 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw5636 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw5636step0 line 95
  19. def OAI.MUB6.Certificate.PairSemantics.raw5636step1 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw5636step2 line 99
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical5636 line 101
  22. def OAI.MUB6.Certificate.PairSemantics.raw5637 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw5637step0 line 120
  24. def OAI.MUB6.Certificate.PairSemantics.raw5637step1 line 122
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5637 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw5638 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw5638step0 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw5638step1 line 141
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5638 line 143
  30. def OAI.MUB6.Certificate.PairSemantics.raw5639 line 156
  31. def OAI.MUB6.Certificate.PairSemantics.raw5639step0 line 158
  32. def OAI.MUB6.Certificate.PairSemantics.raw5639step1 line 160
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5639 line 162
  34. def OAI.MUB6.Certificate.PairSemantics.raw5640 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw5640step0 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw5640step1 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw5640step2 line 181
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5640 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw5641 line 200
  40. def OAI.MUB6.Certificate.PairSemantics.raw5641step0 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw5641step1 line 204
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5641 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw5642 line 219
  44. def OAI.MUB6.Certificate.PairSemantics.raw5642step0 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw5642step1 line 223
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5642 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw5643 line 238
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5643 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw5644 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw5644step0 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw5644step1 line 248
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical5644 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw5645 line 263
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5645 line 265
  55. def OAI.MUB6.Certificate.PairSemantics.raw5646 line 269
  56. def OAI.MUB6.Certificate.PairSemantics.raw5646step0 line 271
  57. def OAI.MUB6.Certificate.PairSemantics.raw5646step1 line 273
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5646 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw5647 line 288
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5647 line 290
  61. def OAI.MUB6.Certificate.PairSemantics.raw5648 line 294
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5648 line 296
  63. def OAI.MUB6.Certificate.PairSemantics.raw5649 line 300
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5649 line 302
  65. def OAI.MUB6.Certificate.PairSemantics.raw5650 line 306
  66. def OAI.MUB6.Certificate.PairSemantics.raw5650step0 line 308
  67. def OAI.MUB6.Certificate.PairSemantics.raw5650step1 line 310
  68. def OAI.MUB6.Certificate.PairSemantics.raw5650step2 line 312
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical5650 line 314
  70. def OAI.MUB6.Certificate.PairSemantics.raw5651 line 331
  71. def OAI.MUB6.Certificate.PairSemantics.raw5651step0 line 333
  72. def OAI.MUB6.Certificate.PairSemantics.raw5651step1 line 335
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5651 line 337
  74. def OAI.MUB6.Certificate.PairSemantics.raw5652 line 351
  75. def OAI.MUB6.Certificate.PairSemantics.raw5652step0 line 353
  76. def OAI.MUB6.Certificate.PairSemantics.raw5652step1 line 355
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical5652 line 357
  78. def OAI.MUB6.Certificate.PairSemantics.raw5653 line 371
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5653 line 373
  80. def OAI.MUB6.Certificate.PairSemantics.raw5654 line 377
  81. def OAI.MUB6.Certificate.PairSemantics.raw5654step0 line 379
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical5654 line 381
  83. def OAI.MUB6.Certificate.PairSemantics.raw5655 line 390
  84. def OAI.MUB6.Certificate.PairSemantics.raw5655step0 line 392
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical5655 line 394
  86. def OAI.MUB6.Certificate.PairSemantics.raw5656 line 403
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5656 line 405
  88. def OAI.MUB6.Certificate.PairSemantics.raw5657 line 409
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5657 line 411
  90. def OAI.MUB6.Certificate.PairSemantics.raw5658 line 415
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical5658 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw5659 line 421
  93. def OAI.MUB6.Certificate.PairSemantics.raw5659step0 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw5659step1 line 425
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical5659 line 427
  96. def OAI.MUB6.Certificate.PairSemantics.raw5660 line 440
  97. def OAI.MUB6.Certificate.PairSemantics.raw5660step0 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw5660step1 line 444
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5660 line 446
  100. def OAI.MUB6.Certificate.PairSemantics.raw5661 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw5661step0 line 461
  102. def OAI.MUB6.Certificate.PairSemantics.raw5661step1 line 463
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5661 line 465
  104. def OAI.MUB6.Certificate.PairSemantics.raw5662 line 478
  105. def OAI.MUB6.Certificate.PairSemantics.raw5662step0 line 480
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical5662 line 482
  107. def OAI.MUB6.Certificate.PairSemantics.raw5663 line 491
  108. def OAI.MUB6.Certificate.PairSemantics.raw5663step0 line 493
  109. def OAI.MUB6.Certificate.PairSemantics.raw5663step1 line 495
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5663 line 497