OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical135.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4320 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw4320step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw4320step1 line 24
  4. def OAI.MUB6.Certificate.PairSemantics.raw4320step2 line 26
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4320 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw4321 line 45
  7. def OAI.MUB6.Certificate.PairSemantics.raw4321step0 line 47
  8. def OAI.MUB6.Certificate.PairSemantics.raw4321step1 line 49
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4321 line 51
  10. def OAI.MUB6.Certificate.PairSemantics.raw4322 line 64
  11. def OAI.MUB6.Certificate.PairSemantics.raw4322step0 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw4322step1 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw4322step2 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4322 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw4323 line 89
  16. def OAI.MUB6.Certificate.PairSemantics.raw4323step0 line 91
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4323 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw4324 line 102
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4324 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw4325 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw4325step0 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw4325step1 line 112
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4325 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw4326 line 127
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4326 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw4327 line 133
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4327 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw4328 line 139
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical4328 line 141
  30. def OAI.MUB6.Certificate.PairSemantics.raw4329 line 145
  31. def OAI.MUB6.Certificate.PairSemantics.raw4329step0 line 147
  32. def OAI.MUB6.Certificate.PairSemantics.raw4329step1 line 149
  33. def OAI.MUB6.Certificate.PairSemantics.raw4329step2 line 151
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4329 line 153
  35. def OAI.MUB6.Certificate.PairSemantics.raw4330 line 170
  36. def OAI.MUB6.Certificate.PairSemantics.raw4330step0 line 172
  37. def OAI.MUB6.Certificate.PairSemantics.raw4330step1 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw4330step2 line 176
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4330 line 178
  40. def OAI.MUB6.Certificate.PairSemantics.raw4331 line 195
  41. def OAI.MUB6.Certificate.PairSemantics.raw4331step0 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw4331step1 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw4331step2 line 201
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4331 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw4332 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw4332step0 line 222
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4332 line 224
  48. def OAI.MUB6.Certificate.PairSemantics.raw4333 line 233
  49. def OAI.MUB6.Certificate.PairSemantics.raw4333step0 line 235
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4333 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw4334 line 246
  52. def OAI.MUB6.Certificate.PairSemantics.raw4334step0 line 248
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4334 line 250
  54. def OAI.MUB6.Certificate.PairSemantics.raw4335 line 259
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4335 line 261
  56. def OAI.MUB6.Certificate.PairSemantics.raw4336 line 265
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4336 line 267
  58. def OAI.MUB6.Certificate.PairSemantics.raw4337 line 271
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4337 line 273
  60. def OAI.MUB6.Certificate.PairSemantics.raw4338 line 277
  61. def OAI.MUB6.Certificate.PairSemantics.raw4338step0 line 279
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4338 line 281
  63. def OAI.MUB6.Certificate.PairSemantics.raw4339 line 290
  64. def OAI.MUB6.Certificate.PairSemantics.raw4339step0 line 292
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4339 line 294
  66. def OAI.MUB6.Certificate.PairSemantics.raw4340 line 303
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4340 line 305
  68. def OAI.MUB6.Certificate.PairSemantics.raw4341 line 309
  69. def OAI.MUB6.Certificate.PairSemantics.raw4341step0 line 311
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4341 line 313
  71. def OAI.MUB6.Certificate.PairSemantics.raw4342 line 322
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4342 line 324
  73. def OAI.MUB6.Certificate.PairSemantics.raw4343 line 328
  74. def OAI.MUB6.Certificate.PairSemantics.raw4343step0 line 330
  75. def OAI.MUB6.Certificate.PairSemantics.raw4343step1 line 332
  76. def OAI.MUB6.Certificate.PairSemantics.raw4343step2 line 334
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4343 line 336
  78. def OAI.MUB6.Certificate.PairSemantics.raw4344 line 353
  79. def OAI.MUB6.Certificate.PairSemantics.raw4344step0 line 355
  80. def OAI.MUB6.Certificate.PairSemantics.raw4344step1 line 357
  81. def OAI.MUB6.Certificate.PairSemantics.raw4344step2 line 359
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4344 line 361
  83. def OAI.MUB6.Certificate.PairSemantics.raw4345 line 378
  84. def OAI.MUB6.Certificate.PairSemantics.raw4345step0 line 380
  85. def OAI.MUB6.Certificate.PairSemantics.raw4345step1 line 382
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4345 line 384
  87. def OAI.MUB6.Certificate.PairSemantics.raw4346 line 397
  88. def OAI.MUB6.Certificate.PairSemantics.raw4346step0 line 399
  89. def OAI.MUB6.Certificate.PairSemantics.raw4346step1 line 401
  90. def OAI.MUB6.Certificate.PairSemantics.raw4346step2 line 403
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical4346 line 405
  92. def OAI.MUB6.Certificate.PairSemantics.raw4347 line 423
  93. def OAI.MUB6.Certificate.PairSemantics.raw4347step0 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw4347step1 line 427
  95. def OAI.MUB6.Certificate.PairSemantics.raw4347step2 line 429
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4347 line 431
  97. def OAI.MUB6.Certificate.PairSemantics.raw4348 line 449
  98. def OAI.MUB6.Certificate.PairSemantics.raw4348step0 line 451
  99. def OAI.MUB6.Certificate.PairSemantics.raw4348step1 line 453
  100. def OAI.MUB6.Certificate.PairSemantics.raw4348step2 line 455
  101. def OAI.MUB6.Certificate.PairSemantics.raw4348step3 line 457
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical4348 line 459
  103. def OAI.MUB6.Certificate.PairSemantics.raw4349 line 481
  104. def OAI.MUB6.Certificate.PairSemantics.raw4349step0 line 483
  105. def OAI.MUB6.Certificate.PairSemantics.raw4349step1 line 485
  106. def OAI.MUB6.Certificate.PairSemantics.raw4349step2 line 487
  107. def OAI.MUB6.Certificate.PairSemantics.raw4349step3 line 489
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical4349 line 491
  109. def OAI.MUB6.Certificate.PairSemantics.raw4350 line 513
  110. def OAI.MUB6.Certificate.PairSemantics.raw4350step0 line 515
  111. def OAI.MUB6.Certificate.PairSemantics.raw4350step1 line 517
  112. def OAI.MUB6.Certificate.PairSemantics.raw4350step2 line 519
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical4350 line 521
  114. def OAI.MUB6.Certificate.PairSemantics.raw4351 line 539
  115. def OAI.MUB6.Certificate.PairSemantics.raw4351step0 line 541
  116. def OAI.MUB6.Certificate.PairSemantics.raw4351step1 line 543
  117. def OAI.MUB6.Certificate.PairSemantics.raw4351step2 line 545
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical4351 line 547