OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical139.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4448 line 19
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4448 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw4449 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4449 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw4450 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw4450step0 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw4450step1 line 35
  8. def OAI.MUB6.Certificate.PairSemantics.raw4450step2 line 37
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4450 line 39
  10. def OAI.MUB6.Certificate.PairSemantics.raw4451 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw4451step0 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw4451step1 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4451 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw4452 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw4452step0 line 77
  16. def OAI.MUB6.Certificate.PairSemantics.raw4452step1 line 79
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4452 line 81
  18. def OAI.MUB6.Certificate.PairSemantics.raw4453 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw4453step0 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw4453step1 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4453 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw4454 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw4454step0 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw4454step1 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4454 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw4455 line 132
  27. def OAI.MUB6.Certificate.PairSemantics.raw4455step0 line 134
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4455 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw4456 line 145
  30. def OAI.MUB6.Certificate.PairSemantics.raw4456step0 line 147
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4456 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw4457 line 158
  33. def OAI.MUB6.Certificate.PairSemantics.raw4457step0 line 160
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4457 line 162
  35. def OAI.MUB6.Certificate.PairSemantics.raw4458 line 171
  36. def OAI.MUB6.Certificate.PairSemantics.raw4458step0 line 173
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4458 line 175
  38. def OAI.MUB6.Certificate.PairSemantics.raw4459 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw4459step0 line 186
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4459 line 188
  41. def OAI.MUB6.Certificate.PairSemantics.raw4460 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw4460step0 line 199
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4460 line 201
  44. def OAI.MUB6.Certificate.PairSemantics.raw4461 line 210
  45. def OAI.MUB6.Certificate.PairSemantics.raw4461step0 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw4461step1 line 214
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4461 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw4462 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw4462step0 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw4462step1 line 233
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4462 line 235
  52. def OAI.MUB6.Certificate.PairSemantics.raw4463 line 248
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4463 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw4464 line 254
  55. def OAI.MUB6.Certificate.PairSemantics.raw4464step0 line 256
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4464 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw4465 line 267
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4465 line 269
  59. def OAI.MUB6.Certificate.PairSemantics.raw4466 line 273
  60. def OAI.MUB6.Certificate.PairSemantics.raw4466step0 line 275
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4466 line 277
  62. def OAI.MUB6.Certificate.PairSemantics.raw4467 line 286
  63. def OAI.MUB6.Certificate.PairSemantics.raw4467step0 line 288
  64. def OAI.MUB6.Certificate.PairSemantics.raw4467step1 line 290
  65. def OAI.MUB6.Certificate.PairSemantics.raw4467step2 line 292
  66. def OAI.MUB6.Certificate.PairSemantics.raw4467step3 line 294
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4467 line 296
  68. def OAI.MUB6.Certificate.PairSemantics.raw4468 line 318
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4468 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw4469 line 324
  71. def OAI.MUB6.Certificate.PairSemantics.raw4469step0 line 326
  72. def OAI.MUB6.Certificate.PairSemantics.raw4469step1 line 328
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical4469 line 330
  74. def OAI.MUB6.Certificate.PairSemantics.raw4470 line 343
  75. def OAI.MUB6.Certificate.PairSemantics.raw4470step0 line 345
  76. def OAI.MUB6.Certificate.PairSemantics.raw4470step1 line 347
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4470 line 349
  78. def OAI.MUB6.Certificate.PairSemantics.raw4471 line 362
  79. def OAI.MUB6.Certificate.PairSemantics.raw4471step0 line 364
  80. def OAI.MUB6.Certificate.PairSemantics.raw4471step1 line 366
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical4471 line 368
  82. def OAI.MUB6.Certificate.PairSemantics.raw4472 line 381
  83. def OAI.MUB6.Certificate.PairSemantics.raw4472step0 line 383
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical4472 line 385
  85. def OAI.MUB6.Certificate.PairSemantics.raw4473 line 394
  86. def OAI.MUB6.Certificate.PairSemantics.raw4473step0 line 396
  87. def OAI.MUB6.Certificate.PairSemantics.raw4473step1 line 398
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4473 line 400
  89. def OAI.MUB6.Certificate.PairSemantics.raw4474 line 413
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4474 line 415
  91. def OAI.MUB6.Certificate.PairSemantics.raw4475 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw4475step0 line 421
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4475 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw4476 line 432
  95. def OAI.MUB6.Certificate.PairSemantics.raw4476step0 line 434
  96. def OAI.MUB6.Certificate.PairSemantics.raw4476step1 line 436
  97. def OAI.MUB6.Certificate.PairSemantics.raw4476step2 line 438
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical4476 line 440
  99. def OAI.MUB6.Certificate.PairSemantics.raw4477 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw4477step0 line 459
  101. def OAI.MUB6.Certificate.PairSemantics.raw4477step1 line 461
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4477 line 463
  103. def OAI.MUB6.Certificate.PairSemantics.raw4478 line 476
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4478 line 478
  105. def OAI.MUB6.Certificate.PairSemantics.raw4479 line 482
  106. def OAI.MUB6.Certificate.PairSemantics.raw4479step0 line 484
  107. def OAI.MUB6.Certificate.PairSemantics.raw4479step1 line 486
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4479 line 488