OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical0.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw0 line 17
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw0step0 line 19
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw0step1 line 21
  4. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw0step2 line 23
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical0 line 25
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw1 line 46
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw1step0 line 48
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw1step1 line 50
  9. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw1step2 line 52
  10. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical1 line 54
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw2 line 75
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw2step0 line 77
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw2step1 line 79
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical2 line 81
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw3 line 98
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw3step0 line 100
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw3step1 line 102
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw3step2 line 104
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical3 line 106
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw4 line 127
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw4step0 line 129
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw4step1 line 131
  23. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical4 line 133
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw5 line 150
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw5step0 line 152
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw5step1 line 154
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw5step2 line 156
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical5 line 158
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw6 line 179
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw6step0 line 181
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw6step1 line 183
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical6 line 185
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw7 line 201
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw7step0 line 203
  35. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical7 line 205
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw8 line 216
  37. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw8step0 line 218
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw8step1 line 220
  39. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical8 line 222
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw9 line 239
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw9step0 line 241
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw9step1 line 243
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw9step2 line 245
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw9step3 line 247
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw9step4 line 249
  46. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical9 line 251
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw10 line 285
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw10step0 line 287
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw10step1 line 289
  50. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical10 line 291
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw11 line 307
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw11step0 line 309
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw11step1 line 311
  54. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw11step2 line 313
  55. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical11 line 315
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw12 line 336
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw12step0 line 338
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw12step1 line 340
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw12step2 line 342
  60. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical12 line 344
  61. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw13 line 367
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw13step0 line 369
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw13step1 line 371
  64. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical13 line 373
  65. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw14 line 389
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw14step0 line 391
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw14step1 line 393
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw14step2 line 395
  69. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw14step3 line 397
  70. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw14step4 line 399
  71. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical14 line 401
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw15 line 435
  73. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw15step0 line 437
  74. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw15step1 line 439
  75. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical15 line 441