OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical2.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw32 line 19
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw32step0 line 21
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw32step1 line 23
  4. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw32step2 line 25
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical32 line 27
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw33 line 48
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw33step0 line 50
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw33step1 line 52
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical33 line 54
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw34 line 70
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw34step0 line 72
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw34step1 line 74
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw34step2 line 76
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical34 line 78
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw35 line 99
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw35step0 line 101
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw35step1 line 103
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical35 line 105
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw36 line 121
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw36step0 line 123
  21. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical36 line 125
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw37 line 136
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw37step0 line 138
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw37step1 line 140
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw37step2 line 142
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw37step3 line 144
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical37 line 146
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw38 line 175
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw38step0 line 177
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw38step1 line 179
  31. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical38 line 181
  32. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw39 line 197
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw39step0 line 199
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw39step1 line 201
  35. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical39 line 203
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw40 line 219
  37. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw40step0 line 221
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw40step1 line 223
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw40step2 line 225
  40. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical40 line 227
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw41 line 248
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw41step0 line 250
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw41step1 line 252
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw41step2 line 254
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw41step3 line 256
  46. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical41 line 258
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw42 line 285
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw42step0 line 287
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw42step1 line 289
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical42 line 291
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw43 line 307
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw43step0 line 309
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw43step1 line 311
  54. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw43step2 line 313
  55. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical43 line 315
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw44 line 337
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw44step0 line 339
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw44step1 line 341
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw44step2 line 343
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw44step3 line 345
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical44 line 347
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw45 line 375
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw45step0 line 377
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw45step1 line 379
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical45 line 381
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw46 line 397
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw46step0 line 399
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw46step1 line 401
  69. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw46step2 line 403
  70. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical46 line 405
  71. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw47 line 426
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw47step0 line 428
  73. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw47step1 line 430
  74. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw47step2 line 432
  75. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw47step3 line 434
  76. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical47 line 436