OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical291.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9312 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw9312step0 line 23
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9312 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw9313 line 34
  5. def OAI.MUB6.Certificate.PairSemantics.raw9313step0 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw9313step1 line 38
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical9313 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw9314 line 53
  9. def OAI.MUB6.Certificate.PairSemantics.raw9314step0 line 55
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9314 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw9315 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw9315step0 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw9315step1 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical9315 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw9316 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw9316step0 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw9316step1 line 90
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9316 line 92
  19. def OAI.MUB6.Certificate.PairSemantics.raw9317 line 106
  20. def OAI.MUB6.Certificate.PairSemantics.raw9317step0 line 108
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9317 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw9318 line 119
  23. def OAI.MUB6.Certificate.PairSemantics.raw9318step0 line 121
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9318 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw9319 line 132
  26. def OAI.MUB6.Certificate.PairSemantics.raw9319step0 line 134
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9319 line 136
  28. def OAI.MUB6.Certificate.PairSemantics.raw9320 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw9320step0 line 147
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9320 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw9321 line 158
  32. def OAI.MUB6.Certificate.PairSemantics.raw9321step0 line 160
  33. def OAI.MUB6.Certificate.PairSemantics.raw9321step1 line 162
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9321 line 164
  35. def OAI.MUB6.Certificate.PairSemantics.raw9322 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw9322step0 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw9322step1 line 181
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9322 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw9323 line 196
  40. def OAI.MUB6.Certificate.PairSemantics.raw9323step0 line 198
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9323 line 200
  42. def OAI.MUB6.Certificate.PairSemantics.raw9324 line 209
  43. def OAI.MUB6.Certificate.PairSemantics.raw9324step0 line 211
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9324 line 213
  45. def OAI.MUB6.Certificate.PairSemantics.raw9325 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw9325step0 line 224
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9325 line 226
  48. def OAI.MUB6.Certificate.PairSemantics.raw9326 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw9326step0 line 237
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9326 line 239
  51. def OAI.MUB6.Certificate.PairSemantics.raw9327 line 248
  52. def OAI.MUB6.Certificate.PairSemantics.raw9327step0 line 250
  53. def OAI.MUB6.Certificate.PairSemantics.raw9327step1 line 252
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9327 line 254
  55. def OAI.MUB6.Certificate.PairSemantics.raw9328 line 267
  56. def OAI.MUB6.Certificate.PairSemantics.raw9328step0 line 269
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9328 line 271
  58. def OAI.MUB6.Certificate.PairSemantics.raw9329 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw9329step0 line 282
  60. def OAI.MUB6.Certificate.PairSemantics.raw9329step1 line 284
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9329 line 286
  62. def OAI.MUB6.Certificate.PairSemantics.raw9330 line 300
  63. def OAI.MUB6.Certificate.PairSemantics.raw9330step0 line 302
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical9330 line 304
  65. def OAI.MUB6.Certificate.PairSemantics.raw9331 line 313
  66. def OAI.MUB6.Certificate.PairSemantics.raw9331step0 line 315
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9331 line 317
  68. def OAI.MUB6.Certificate.PairSemantics.raw9332 line 326
  69. def OAI.MUB6.Certificate.PairSemantics.raw9332step0 line 328
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9332 line 330
  71. def OAI.MUB6.Certificate.PairSemantics.raw9333 line 339
  72. def OAI.MUB6.Certificate.PairSemantics.raw9333step0 line 341
  73. def OAI.MUB6.Certificate.PairSemantics.raw9333step1 line 343
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical9333 line 345
  75. def OAI.MUB6.Certificate.PairSemantics.raw9334 line 358
  76. def OAI.MUB6.Certificate.PairSemantics.raw9334step0 line 360
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9334 line 362
  78. def OAI.MUB6.Certificate.PairSemantics.raw9335 line 371
  79. def OAI.MUB6.Certificate.PairSemantics.raw9335step0 line 373
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical9335 line 375
  81. def OAI.MUB6.Certificate.PairSemantics.raw9336 line 384
  82. def OAI.MUB6.Certificate.PairSemantics.raw9336step0 line 386
  83. def OAI.MUB6.Certificate.PairSemantics.raw9336step1 line 388
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9336 line 390
  85. def OAI.MUB6.Certificate.PairSemantics.raw9337 line 403
  86. def OAI.MUB6.Certificate.PairSemantics.raw9337step0 line 405
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9337 line 407
  88. def OAI.MUB6.Certificate.PairSemantics.raw9338 line 416
  89. def OAI.MUB6.Certificate.PairSemantics.raw9338step0 line 418
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical9338 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw9339 line 429
  92. def OAI.MUB6.Certificate.PairSemantics.raw9339step0 line 431
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical9339 line 433
  94. def OAI.MUB6.Certificate.PairSemantics.raw9340 line 442
  95. def OAI.MUB6.Certificate.PairSemantics.raw9340step0 line 444
  96. def OAI.MUB6.Certificate.PairSemantics.raw9340step1 line 446
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical9340 line 448
  98. def OAI.MUB6.Certificate.PairSemantics.raw9341 line 461
  99. def OAI.MUB6.Certificate.PairSemantics.raw9341step0 line 463
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical9341 line 465
  101. def OAI.MUB6.Certificate.PairSemantics.raw9342 line 474
  102. def OAI.MUB6.Certificate.PairSemantics.raw9342step0 line 476
  103. def OAI.MUB6.Certificate.PairSemantics.raw9342step1 line 478
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical9342 line 480
  105. def OAI.MUB6.Certificate.PairSemantics.raw9343 line 493
  106. def OAI.MUB6.Certificate.PairSemantics.raw9343step0 line 495
  107. def OAI.MUB6.Certificate.PairSemantics.raw9343step1 line 497
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical9343 line 499