OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical156.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4992 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw4992step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw4992step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4992 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw4993 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw4993step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw4993step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4993 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw4994 line 59
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical4994 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw4995 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw4995step0 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw4995step1 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4995 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw4996 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw4996step0 line 86
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4996 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw4997 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw4997step0 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4997 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw4998 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw4998step0 line 112
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4998 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw4999 line 123
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4999 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw5000 line 129
  27. def OAI.MUB6.Certificate.PairSemantics.raw5000step0 line 131
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5000 line 133
  29. def OAI.MUB6.Certificate.PairSemantics.raw5001 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw5001step0 line 144
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5001 line 146
  32. def OAI.MUB6.Certificate.PairSemantics.raw5002 line 155
  33. def OAI.MUB6.Certificate.PairSemantics.raw5002step0 line 157
  34. def OAI.MUB6.Certificate.PairSemantics.raw5002step1 line 159
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5002 line 161
  36. def OAI.MUB6.Certificate.PairSemantics.raw5003 line 174
  37. def OAI.MUB6.Certificate.PairSemantics.raw5003step0 line 176
  38. def OAI.MUB6.Certificate.PairSemantics.raw5003step1 line 178
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical5003 line 180
  40. def OAI.MUB6.Certificate.PairSemantics.raw5004 line 193
  41. def OAI.MUB6.Certificate.PairSemantics.raw5004step0 line 195
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5004 line 197
  43. def OAI.MUB6.Certificate.PairSemantics.raw5005 line 206
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5005 line 208
  45. def OAI.MUB6.Certificate.PairSemantics.raw5006 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw5006step0 line 214
  47. def OAI.MUB6.Certificate.PairSemantics.raw5006step1 line 216
  48. def OAI.MUB6.Certificate.PairSemantics.raw5006step2 line 218
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5006 line 220
  50. def OAI.MUB6.Certificate.PairSemantics.raw5007 line 237
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5007 line 239
  52. def OAI.MUB6.Certificate.PairSemantics.raw5008 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw5008step0 line 245
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5008 line 247
  55. def OAI.MUB6.Certificate.PairSemantics.raw5009 line 256
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5009 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw5010 line 262
  58. def OAI.MUB6.Certificate.PairSemantics.raw5010step0 line 264
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5010 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw5011 line 275
  61. def OAI.MUB6.Certificate.PairSemantics.raw5011step0 line 277
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5011 line 279
  63. def OAI.MUB6.Certificate.PairSemantics.raw5012 line 288
  64. def OAI.MUB6.Certificate.PairSemantics.raw5012step0 line 290
  65. def OAI.MUB6.Certificate.PairSemantics.raw5012step1 line 292
  66. def OAI.MUB6.Certificate.PairSemantics.raw5012step2 line 294
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5012 line 296
  68. def OAI.MUB6.Certificate.PairSemantics.raw5013 line 313
  69. def OAI.MUB6.Certificate.PairSemantics.raw5013step0 line 315
  70. def OAI.MUB6.Certificate.PairSemantics.raw5013step1 line 317
  71. def OAI.MUB6.Certificate.PairSemantics.raw5013step2 line 319
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5013 line 321
  73. def OAI.MUB6.Certificate.PairSemantics.raw5014 line 338
  74. def OAI.MUB6.Certificate.PairSemantics.raw5014step0 line 340
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5014 line 342
  76. def OAI.MUB6.Certificate.PairSemantics.raw5015 line 351
  77. def OAI.MUB6.Certificate.PairSemantics.raw5015step0 line 353
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5015 line 355
  79. def OAI.MUB6.Certificate.PairSemantics.raw5016 line 364
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical5016 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw5017 line 370
  82. def OAI.MUB6.Certificate.PairSemantics.raw5017step0 line 372
  83. def OAI.MUB6.Certificate.PairSemantics.raw5017step1 line 374
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5017 line 376
  85. def OAI.MUB6.Certificate.PairSemantics.raw5018 line 389
  86. def OAI.MUB6.Certificate.PairSemantics.raw5018step0 line 391
  87. def OAI.MUB6.Certificate.PairSemantics.raw5018step1 line 393
  88. def OAI.MUB6.Certificate.PairSemantics.raw5018step2 line 395
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5018 line 397
  90. def OAI.MUB6.Certificate.PairSemantics.raw5019 line 414
  91. def OAI.MUB6.Certificate.PairSemantics.raw5019step0 line 416
  92. def OAI.MUB6.Certificate.PairSemantics.raw5019step1 line 418
  93. def OAI.MUB6.Certificate.PairSemantics.raw5019step2 line 420
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical5019 line 422
  95. def OAI.MUB6.Certificate.PairSemantics.raw5020 line 439
  96. def OAI.MUB6.Certificate.PairSemantics.raw5020step0 line 441
  97. def OAI.MUB6.Certificate.PairSemantics.raw5020step1 line 443
  98. def OAI.MUB6.Certificate.PairSemantics.raw5020step2 line 445
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical5020 line 447
  100. def OAI.MUB6.Certificate.PairSemantics.raw5021 line 464
  101. def OAI.MUB6.Certificate.PairSemantics.raw5021step0 line 466
  102. def OAI.MUB6.Certificate.PairSemantics.raw5021step1 line 468
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical5021 line 470
  104. def OAI.MUB6.Certificate.PairSemantics.raw5022 line 483
  105. def OAI.MUB6.Certificate.PairSemantics.raw5022step0 line 485
  106. def OAI.MUB6.Certificate.PairSemantics.raw5022step1 line 487
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical5022 line 489
  108. def OAI.MUB6.Certificate.PairSemantics.raw5023 line 502
  109. def OAI.MUB6.Certificate.PairSemantics.raw5023step0 line 504
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5023 line 506