OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical137.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4384 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4384step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw4384step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4384 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw4385 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw4385step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw4385step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical4385 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw4386 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw4386step0 line 60
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4386 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw4387 line 71
  13. def OAI.MUB6.Certificate.PairSemantics.raw4387step0 line 73
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4387 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw4388 line 84
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4388 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw4389 line 90
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4389 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw4390 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw4390step0 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4390 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw4391 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw4391step0 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw4391step1 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw4391step2 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical4391 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw4392 line 134
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4392 line 136
  29. def OAI.MUB6.Certificate.PairSemantics.raw4393 line 140
  30. def OAI.MUB6.Certificate.PairSemantics.raw4393step0 line 142
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical4393 line 144
  32. def OAI.MUB6.Certificate.PairSemantics.raw4394 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw4394step0 line 155
  34. def OAI.MUB6.Certificate.PairSemantics.raw4394step1 line 157
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4394 line 159
  36. def OAI.MUB6.Certificate.PairSemantics.raw4395 line 172
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4395 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw4396 line 178
  39. def OAI.MUB6.Certificate.PairSemantics.raw4396step0 line 180
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4396 line 182
  41. def OAI.MUB6.Certificate.PairSemantics.raw4397 line 191
  42. def OAI.MUB6.Certificate.PairSemantics.raw4397step0 line 193
  43. def OAI.MUB6.Certificate.PairSemantics.raw4397step1 line 195
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4397 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw4398 line 210
  46. def OAI.MUB6.Certificate.PairSemantics.raw4398step0 line 212
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4398 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw4399 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw4399step0 line 225
  50. def OAI.MUB6.Certificate.PairSemantics.raw4399step1 line 227
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4399 line 229
  52. def OAI.MUB6.Certificate.PairSemantics.raw4400 line 242
  53. def OAI.MUB6.Certificate.PairSemantics.raw4400step0 line 244
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4400 line 246
  55. def OAI.MUB6.Certificate.PairSemantics.raw4401 line 255
  56. def OAI.MUB6.Certificate.PairSemantics.raw4401step0 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw4401step1 line 259
  58. def OAI.MUB6.Certificate.PairSemantics.raw4401step2 line 261
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4401 line 263
  60. def OAI.MUB6.Certificate.PairSemantics.raw4402 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw4402step0 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw4402step1 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw4402step2 line 286
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4402 line 288
  65. def OAI.MUB6.Certificate.PairSemantics.raw4403 line 305
  66. def OAI.MUB6.Certificate.PairSemantics.raw4403step0 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw4403step1 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw4403step2 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4403 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw4404 line 330
  71. def OAI.MUB6.Certificate.PairSemantics.raw4404step0 line 332
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4404 line 334
  73. def OAI.MUB6.Certificate.PairSemantics.raw4405 line 343
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical4405 line 345
  75. def OAI.MUB6.Certificate.PairSemantics.raw4406 line 349
  76. def OAI.MUB6.Certificate.PairSemantics.raw4406step0 line 351
  77. def OAI.MUB6.Certificate.PairSemantics.raw4406step1 line 353
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical4406 line 355
  79. def OAI.MUB6.Certificate.PairSemantics.raw4407 line 368
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4407 line 370
  81. def OAI.MUB6.Certificate.PairSemantics.raw4408 line 374
  82. def OAI.MUB6.Certificate.PairSemantics.raw4408step0 line 376
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4408 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw4409 line 387
  85. def OAI.MUB6.Certificate.PairSemantics.raw4409step0 line 389
  86. def OAI.MUB6.Certificate.PairSemantics.raw4409step1 line 391
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical4409 line 393
  88. def OAI.MUB6.Certificate.PairSemantics.raw4410 line 406
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4410 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw4411 line 412
  91. def OAI.MUB6.Certificate.PairSemantics.raw4411step0 line 414
  92. def OAI.MUB6.Certificate.PairSemantics.raw4411step1 line 416
  93. def OAI.MUB6.Certificate.PairSemantics.raw4411step2 line 418
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4411 line 420
  95. def OAI.MUB6.Certificate.PairSemantics.raw4412 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw4412step0 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw4412step1 line 441
  98. def OAI.MUB6.Certificate.PairSemantics.raw4412step2 line 443
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical4412 line 445
  100. def OAI.MUB6.Certificate.PairSemantics.raw4413 line 462
  101. def OAI.MUB6.Certificate.PairSemantics.raw4413step0 line 464
  102. def OAI.MUB6.Certificate.PairSemantics.raw4413step1 line 466
  103. def OAI.MUB6.Certificate.PairSemantics.raw4413step2 line 468
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical4413 line 470
  105. def OAI.MUB6.Certificate.PairSemantics.raw4414 line 487
  106. def OAI.MUB6.Certificate.PairSemantics.raw4414step0 line 489
  107. def OAI.MUB6.Certificate.PairSemantics.raw4414step1 line 491
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4414 line 493
  109. def OAI.MUB6.Certificate.PairSemantics.raw4415 line 506
  110. def OAI.MUB6.Certificate.PairSemantics.raw4415step0 line 508
  111. def OAI.MUB6.Certificate.PairSemantics.raw4415step1 line 510
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical4415 line 512