OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical3.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw48 line 16
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw48step0 line 18
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw48step1 line 20
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical48 line 22
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw49 line 38
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw49step0 line 40
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw49step1 line 42
  8. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw49step2 line 44
  9. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical49 line 46
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw50 line 68
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw50step0 line 70
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw50step1 line 72
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical50 line 74
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw51 line 90
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw51step0 line 92
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw51step1 line 94
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw51step2 line 96
  18. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw51step3 line 98
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw51step4 line 100
  20. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical51 line 102
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw52 line 136
  22. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw52step0 line 138
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw52step1 line 140
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw52step2 line 142
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw52step3 line 144
  26. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical52 line 146
  27. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw53 line 173
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw53step0 line 175
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw53step1 line 177
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw53step2 line 179
  31. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical53 line 181
  32. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw54 line 202
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw54step0 line 204
  34. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical54 line 206
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw55 line 217
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw55step0 line 219
  37. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw55step1 line 221
  38. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical55 line 223
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw56 line 239
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw56step0 line 241
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw56step1 line 243
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw56step2 line 245
  43. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical56 line 247
  44. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw57 line 269
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw57step0 line 271
  46. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw57step1 line 273
  47. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical57 line 275
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw58 line 291
  49. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw58step0 line 293
  50. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw58step1 line 295
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw58step2 line 297
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw58step3 line 299
  53. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw58step4 line 301
  54. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical58 line 303
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw59 line 337
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw59step0 line 339
  57. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw59step1 line 341
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw59step2 line 343
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw59step3 line 345
  60. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical59 line 347
  61. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw60 line 374
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw60step0 line 376
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw60step1 line 378
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw60step2 line 380
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical60 line 382
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw61 line 403
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw61step0 line 405
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw61step1 line 407
  69. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical61 line 409
  70. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw62 line 425
  71. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw62step0 line 427
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw62step1 line 429
  73. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical62 line 431
  74. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw63 line 447
  75. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw63step0 line 449
  76. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw63step1 line 451
  77. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw63step2 line 453
  78. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical63 line 455