OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical292.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9344 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw9344step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9344 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw9345 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw9345step0 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw9345step1 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw9345step2 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical9345 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw9346 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw9346step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw9346step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9346 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw9347 line 77
  14. def OAI.MUB6.Certificate.PairSemantics.raw9347step0 line 79
  15. def OAI.MUB6.Certificate.PairSemantics.raw9347step1 line 81
  16. def OAI.MUB6.Certificate.PairSemantics.raw9347step2 line 83
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical9347 line 85
  18. def OAI.MUB6.Certificate.PairSemantics.raw9348 line 103
  19. def OAI.MUB6.Certificate.PairSemantics.raw9348step0 line 105
  20. def OAI.MUB6.Certificate.PairSemantics.raw9348step1 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw9348step2 line 109
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical9348 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw9349 line 129
  24. def OAI.MUB6.Certificate.PairSemantics.raw9349step0 line 131
  25. def OAI.MUB6.Certificate.PairSemantics.raw9349step1 line 133
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical9349 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw9350 line 148
  28. def OAI.MUB6.Certificate.PairSemantics.raw9350step0 line 150
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9350 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw9351 line 161
  31. def OAI.MUB6.Certificate.PairSemantics.raw9351step0 line 163
  32. def OAI.MUB6.Certificate.PairSemantics.raw9351step1 line 165
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9351 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw9352 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw9352step0 line 182
  36. def OAI.MUB6.Certificate.PairSemantics.raw9352step1 line 184
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9352 line 186
  38. def OAI.MUB6.Certificate.PairSemantics.raw9353 line 199
  39. def OAI.MUB6.Certificate.PairSemantics.raw9353step0 line 201
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9353 line 203
  41. def OAI.MUB6.Certificate.PairSemantics.raw9354 line 212
  42. def OAI.MUB6.Certificate.PairSemantics.raw9354step0 line 214
  43. def OAI.MUB6.Certificate.PairSemantics.raw9354step1 line 216
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical9354 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw9355 line 231
  46. def OAI.MUB6.Certificate.PairSemantics.raw9355step0 line 233
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9355 line 235
  48. def OAI.MUB6.Certificate.PairSemantics.raw9356 line 244
  49. def OAI.MUB6.Certificate.PairSemantics.raw9356step0 line 246
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9356 line 248
  51. def OAI.MUB6.Certificate.PairSemantics.raw9357 line 257
  52. def OAI.MUB6.Certificate.PairSemantics.raw9357step0 line 259
  53. def OAI.MUB6.Certificate.PairSemantics.raw9357step1 line 261
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical9357 line 263
  55. def OAI.MUB6.Certificate.PairSemantics.raw9358 line 276
  56. def OAI.MUB6.Certificate.PairSemantics.raw9358step0 line 278
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical9358 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw9359 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw9359step0 line 291
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical9359 line 293
  61. def OAI.MUB6.Certificate.PairSemantics.raw9360 line 302
  62. def OAI.MUB6.Certificate.PairSemantics.raw9360step0 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw9360step1 line 306
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical9360 line 308
  65. def OAI.MUB6.Certificate.PairSemantics.raw9361 line 321
  66. def OAI.MUB6.Certificate.PairSemantics.raw9361step0 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw9361step1 line 325
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9361 line 327
  69. def OAI.MUB6.Certificate.PairSemantics.raw9362 line 340
  70. def OAI.MUB6.Certificate.PairSemantics.raw9362step0 line 342
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical9362 line 344
  72. def OAI.MUB6.Certificate.PairSemantics.raw9363 line 353
  73. def OAI.MUB6.Certificate.PairSemantics.raw9363step0 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw9363step1 line 357
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9363 line 359
  76. def OAI.MUB6.Certificate.PairSemantics.raw9364 line 372
  77. def OAI.MUB6.Certificate.PairSemantics.raw9364step0 line 374
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9364 line 376
  79. def OAI.MUB6.Certificate.PairSemantics.raw9365 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw9365step0 line 387
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9365 line 389
  82. def OAI.MUB6.Certificate.PairSemantics.raw9366 line 398
  83. def OAI.MUB6.Certificate.PairSemantics.raw9366step0 line 400
  84. def OAI.MUB6.Certificate.PairSemantics.raw9366step1 line 402
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical9366 line 404
  86. def OAI.MUB6.Certificate.PairSemantics.raw9367 line 417
  87. def OAI.MUB6.Certificate.PairSemantics.raw9367step0 line 419
  88. def OAI.MUB6.Certificate.PairSemantics.raw9367step1 line 421
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical9367 line 423
  90. def OAI.MUB6.Certificate.PairSemantics.raw9368 line 436
  91. def OAI.MUB6.Certificate.PairSemantics.raw9368step0 line 438
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9368 line 440
  93. def OAI.MUB6.Certificate.PairSemantics.raw9369 line 449
  94. def OAI.MUB6.Certificate.PairSemantics.raw9369step0 line 451
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9369 line 453
  96. def OAI.MUB6.Certificate.PairSemantics.raw9370 line 462
  97. def OAI.MUB6.Certificate.PairSemantics.raw9370step0 line 464
  98. def OAI.MUB6.Certificate.PairSemantics.raw9370step1 line 466
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical9370 line 468
  100. def OAI.MUB6.Certificate.PairSemantics.raw9371 line 481
  101. def OAI.MUB6.Certificate.PairSemantics.raw9371step0 line 483
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9371 line 485
  103. def OAI.MUB6.Certificate.PairSemantics.raw9372 line 494
  104. def OAI.MUB6.Certificate.PairSemantics.raw9372step0 line 496
  105. def OAI.MUB6.Certificate.PairSemantics.raw9372step1 line 498
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical9372 line 500
  107. def OAI.MUB6.Certificate.PairSemantics.raw9373 line 513
  108. def OAI.MUB6.Certificate.PairSemantics.raw9373step0 line 515
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical9373 line 517
  110. def OAI.MUB6.Certificate.PairSemantics.raw9374 line 526
  111. def OAI.MUB6.Certificate.PairSemantics.raw9374step0 line 528
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical9374 line 530
  113. def OAI.MUB6.Certificate.PairSemantics.raw9375 line 539
  114. def OAI.MUB6.Certificate.PairSemantics.raw9375step0 line 541
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical9375 line 543