OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical4.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw64 line 20
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw64step0 line 22
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw64step1 line 24
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical64 line 26
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw65 line 42
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw65step0 line 44
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw65step1 line 46
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw65step2 line 48
  9. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw65step3 line 50
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw65step4 line 52
  11. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical65 line 54
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw66 line 88
  13. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw66step0 line 90
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw66step1 line 92
  15. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical66 line 94
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw67 line 110
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw67step0 line 112
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw67step1 line 114
  19. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical67 line 116
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw68 line 132
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw68step0 line 134
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw68step1 line 136
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw68step2 line 138
  24. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical68 line 140
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw69 line 162
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw69step0 line 164
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw69step1 line 166
  28. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical69 line 168
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw70 line 184
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw70step0 line 186
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw70step1 line 188
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical70 line 190
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw71 line 206
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw71step0 line 208
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw71step1 line 210
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw71step2 line 212
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical71 line 214
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw72 line 236
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw72step0 line 238
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw72step1 line 240
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw72step2 line 242
  42. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical72 line 244
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw73 line 265
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw73step0 line 267
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw73step1 line 269
  46. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical73 line 271
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw74 line 287
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw74step0 line 289
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw74step1 line 291
  50. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw74step2 line 293
  51. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical74 line 295
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw75 line 317
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw75step0 line 319
  54. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw75step1 line 321
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw75step2 line 323
  56. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical75 line 325
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw76 line 346
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw76step0 line 348
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw76step1 line 350
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw76step2 line 352
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical76 line 354
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw77 line 375
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw77step0 line 377
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw77step1 line 379
  65. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw77step2 line 381
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw77step3 line 383
  67. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical77 line 385
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw78 line 413
  69. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw78step0 line 415
  70. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw78step1 line 417
  71. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw78step2 line 419
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw78step3 line 421
  73. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical78 line 423
  74. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw79 line 451
  75. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw79step0 line 453
  76. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw79step1 line 455
  77. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw79step2 line 457
  78. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical79 line 459