OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical7.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw112 line 18
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw112step0 line 20
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw112step1 line 22
  4. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw112step2 line 24
  5. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical112 line 26
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw113 line 47
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw113step0 line 49
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw113step1 line 51
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical113 line 53
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw114 line 69
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw114step0 line 71
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw114step1 line 73
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw114step2 line 75
  14. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical114 line 77
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw115 line 100
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw115step0 line 102
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw115step1 line 104
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical115 line 106
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw116 line 122
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw116step0 line 124
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw116step1 line 126
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw116step2 line 128
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw116step3 line 130
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw116step4 line 132
  25. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical116 line 134
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw117 line 168
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw117step0 line 170
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical117 line 172
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw118 line 182
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw118step0 line 184
  31. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical118 line 186
  32. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw119 line 196
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw119step0 line 198
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw119step1 line 200
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw119step2 line 202
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw119step3 line 204
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical119 line 206
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120 line 235
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120step0 line 237
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120step1 line 239
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120step2 line 241
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120step3 line 243
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120step4 line 245
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw120step5 line 247
  45. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical120 line 249
  46. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw121 line 289
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw121step0 line 291
  48. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical121 line 293
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw122 line 303
  50. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw122step0 line 305
  51. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical122 line 307
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw123 line 317
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw123step0 line 319
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical123 line 321
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw124 line 331
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw124step0 line 333
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw124step1 line 335
  58. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical124 line 337
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw125 line 353
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw125step0 line 355
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical125 line 357
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw126 line 367
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw126step0 line 369
  64. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical126 line 371
  65. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw127 line 381
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw127step0 line 383
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw127step1 line 385
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw127step2 line 387
  69. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw127step3 line 389
  70. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw127step4 line 391
  71. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical127 line 393