OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical5.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw80 line 19
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw80step0 line 21
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw80step1 line 23
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical80 line 25
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw81 line 41
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw81step0 line 43
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw81step1 line 45
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw81step2 line 47
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical81 line 49
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw82 line 72
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw82step0 line 74
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw82step1 line 76
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical82 line 78
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw83 line 94
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw83step0 line 96
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw83step1 line 98
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw83step2 line 100
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw83step3 line 102
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical83 line 104
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw84 line 133
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw84step0 line 135
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw84step1 line 137
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw84step2 line 139
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical84 line 141
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw85 line 163
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw85step0 line 165
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw85step1 line 167
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw85step2 line 169
  29. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical85 line 171
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw86 line 193
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw86step0 line 195
  32. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw86step1 line 197
  33. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical86 line 199
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw87 line 215
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw87step0 line 217
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw87step1 line 219
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical87 line 221
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw88 line 237
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw88step0 line 239
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw88step1 line 241
  41. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical88 line 243
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw89 line 259
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw89step0 line 261
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw89step1 line 263
  45. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical89 line 265
  46. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw90 line 281
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw90step0 line 283
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw90step1 line 285
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw90step2 line 287
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical90 line 289
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw91 line 311
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw91step0 line 313
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw91step1 line 315
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical91 line 317
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw92 line 333
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw92step0 line 335
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw92step1 line 337
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw92step2 line 339
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw92step3 line 341
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw92step4 line 343
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical92 line 345
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw93 line 379
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw93step0 line 381
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw93step1 line 383
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical93 line 385
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw94 line 401
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw94step0 line 403
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw94step1 line 405
  69. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical94 line 407
  70. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw95 line 423
  71. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw95step0 line 425
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw95step1 line 427
  73. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw95step2 line 429
  74. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical95 line 431