OAI/Analysis/MutuallyUnbiased/PairTargets/ExtraCanonical6.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw96 line 17
  2. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw96step0 line 19
  3. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw96step1 line 21
  4. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical96 line 23
  5. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw97 line 39
  6. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw97step0 line 41
  7. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw97step1 line 43
  8. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical97 line 45
  9. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw98 line 61
  10. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw98step0 line 63
  11. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw98step1 line 65
  12. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw98step2 line 67
  13. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical98 line 69
  14. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw99 line 91
  15. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw99step0 line 93
  16. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw99step1 line 95
  17. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw99step2 line 97
  18. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical99 line 99
  19. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw100 line 120
  20. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw100step0 line 122
  21. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw100step1 line 124
  22. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical100 line 126
  23. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw101 line 142
  24. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw101step0 line 144
  25. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw101step1 line 146
  26. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw101step2 line 148
  27. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical101 line 150
  28. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw102 line 172
  29. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw102step0 line 174
  30. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw102step1 line 176
  31. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw102step2 line 178
  32. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical102 line 180
  33. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw103 line 201
  34. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw103step0 line 203
  35. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw103step1 line 205
  36. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw103step2 line 207
  37. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical103 line 209
  38. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw104 line 230
  39. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw104step0 line 232
  40. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw104step1 line 234
  41. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw104step2 line 236
  42. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw104step3 line 238
  43. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw104step4 line 240
  44. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical104 line 242
  45. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw105 line 276
  46. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw105step0 line 278
  47. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw105step1 line 280
  48. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw105step2 line 282
  49. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical105 line 284
  50. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw106 line 306
  51. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw106step0 line 308
  52. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw106step1 line 310
  53. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical106 line 312
  54. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw107 line 328
  55. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw107step0 line 330
  56. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw107step1 line 332
  57. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical107 line 334
  58. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw108 line 350
  59. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw108step0 line 352
  60. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw108step1 line 354
  61. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical108 line 356
  62. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw109 line 372
  63. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw109step0 line 374
  64. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw109step1 line 376
  65. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical109 line 378
  66. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw110 line 394
  67. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw110step0 line 396
  68. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw110step1 line 398
  69. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw110step2 line 400
  70. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical110 line 402
  71. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw111 line 425
  72. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw111step0 line 427
  73. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw111step1 line 429
  74. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw111step2 line 431
  75. def OAI.MUB6.Certificate.PairTargetSemantics.extraRaw111step3 line 433
  76. theorem OAI.MUB6.Certificate.PairTargetSemantics.extraCanonical111 line 435