OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical245.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7840 line 20
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical7840 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw7841 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw7841step0 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw7841step1 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical7841 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw7842 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7842 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw7843 line 51
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7843 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw7844 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw7844step0 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw7844step1 line 61
  14. def OAI.MUB6.Certificate.PairSemantics.raw7844step2 line 63
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7844 line 65
  16. def OAI.MUB6.Certificate.PairSemantics.raw7845 line 82
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7845 line 84
  18. def OAI.MUB6.Certificate.PairSemantics.raw7846 line 88
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7846 line 90
  20. def OAI.MUB6.Certificate.PairSemantics.raw7847 line 94
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7847 line 96
  22. def OAI.MUB6.Certificate.PairSemantics.raw7848 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw7848step0 line 102
  24. def OAI.MUB6.Certificate.PairSemantics.raw7848step1 line 104
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical7848 line 106
  26. def OAI.MUB6.Certificate.PairSemantics.raw7849 line 119
  27. def OAI.MUB6.Certificate.PairSemantics.raw7849step0 line 121
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7849 line 123
  29. def OAI.MUB6.Certificate.PairSemantics.raw7850 line 132
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7850 line 134
  31. def OAI.MUB6.Certificate.PairSemantics.raw7851 line 138
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7851 line 140
  33. def OAI.MUB6.Certificate.PairSemantics.raw7852 line 144
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7852 line 146
  35. def OAI.MUB6.Certificate.PairSemantics.raw7853 line 150
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7853 line 152
  37. def OAI.MUB6.Certificate.PairSemantics.raw7854 line 156
  38. def OAI.MUB6.Certificate.PairSemantics.raw7854step0 line 158
  39. def OAI.MUB6.Certificate.PairSemantics.raw7854step1 line 160
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7854 line 162
  41. def OAI.MUB6.Certificate.PairSemantics.raw7855 line 175
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7855 line 177
  43. def OAI.MUB6.Certificate.PairSemantics.raw7856 line 181
  44. def OAI.MUB6.Certificate.PairSemantics.raw7856step0 line 183
  45. def OAI.MUB6.Certificate.PairSemantics.raw7856step1 line 185
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical7856 line 187
  47. def OAI.MUB6.Certificate.PairSemantics.raw7857 line 200
  48. def OAI.MUB6.Certificate.PairSemantics.raw7857step0 line 202
  49. def OAI.MUB6.Certificate.PairSemantics.raw7857step1 line 204
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7857 line 206
  51. def OAI.MUB6.Certificate.PairSemantics.raw7858 line 219
  52. def OAI.MUB6.Certificate.PairSemantics.raw7858step0 line 221
  53. def OAI.MUB6.Certificate.PairSemantics.raw7858step1 line 223
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7858 line 225
  55. def OAI.MUB6.Certificate.PairSemantics.raw7859 line 238
  56. def OAI.MUB6.Certificate.PairSemantics.raw7859step0 line 240
  57. def OAI.MUB6.Certificate.PairSemantics.raw7859step1 line 242
  58. def OAI.MUB6.Certificate.PairSemantics.raw7859step2 line 244
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7859 line 246
  60. def OAI.MUB6.Certificate.PairSemantics.raw7860 line 263
  61. def OAI.MUB6.Certificate.PairSemantics.raw7860step0 line 265
  62. def OAI.MUB6.Certificate.PairSemantics.raw7860step1 line 267
  63. def OAI.MUB6.Certificate.PairSemantics.raw7860step2 line 269
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical7860 line 271
  65. def OAI.MUB6.Certificate.PairSemantics.raw7861 line 288
  66. def OAI.MUB6.Certificate.PairSemantics.raw7861step0 line 290
  67. def OAI.MUB6.Certificate.PairSemantics.raw7861step1 line 292
  68. def OAI.MUB6.Certificate.PairSemantics.raw7861step2 line 294
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7861 line 296
  70. def OAI.MUB6.Certificate.PairSemantics.raw7862 line 314
  71. def OAI.MUB6.Certificate.PairSemantics.raw7862step0 line 316
  72. def OAI.MUB6.Certificate.PairSemantics.raw7862step1 line 318
  73. def OAI.MUB6.Certificate.PairSemantics.raw7862step2 line 320
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7862 line 322
  75. def OAI.MUB6.Certificate.PairSemantics.raw7863 line 340
  76. def OAI.MUB6.Certificate.PairSemantics.raw7863step0 line 342
  77. def OAI.MUB6.Certificate.PairSemantics.raw7863step1 line 344
  78. def OAI.MUB6.Certificate.PairSemantics.raw7863step2 line 346
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical7863 line 348
  80. def OAI.MUB6.Certificate.PairSemantics.raw7864 line 366
  81. def OAI.MUB6.Certificate.PairSemantics.raw7864step0 line 368
  82. def OAI.MUB6.Certificate.PairSemantics.raw7864step1 line 370
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7864 line 372
  84. def OAI.MUB6.Certificate.PairSemantics.raw7865 line 385
  85. def OAI.MUB6.Certificate.PairSemantics.raw7865step0 line 387
  86. def OAI.MUB6.Certificate.PairSemantics.raw7865step1 line 389
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7865 line 391
  88. def OAI.MUB6.Certificate.PairSemantics.raw7866 line 404
  89. def OAI.MUB6.Certificate.PairSemantics.raw7866step0 line 406
  90. def OAI.MUB6.Certificate.PairSemantics.raw7866step1 line 408
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7866 line 410
  92. def OAI.MUB6.Certificate.PairSemantics.raw7867 line 423
  93. def OAI.MUB6.Certificate.PairSemantics.raw7867step0 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw7867step1 line 427
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7867 line 429
  96. def OAI.MUB6.Certificate.PairSemantics.raw7868 line 442
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7868 line 444
  98. def OAI.MUB6.Certificate.PairSemantics.raw7869 line 448
  99. def OAI.MUB6.Certificate.PairSemantics.raw7869step0 line 450
  100. def OAI.MUB6.Certificate.PairSemantics.raw7869step1 line 452
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7869 line 454
  102. def OAI.MUB6.Certificate.PairSemantics.raw7870 line 467
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7870 line 469
  104. def OAI.MUB6.Certificate.PairSemantics.raw7871 line 473
  105. def OAI.MUB6.Certificate.PairSemantics.raw7871step0 line 475
  106. def OAI.MUB6.Certificate.PairSemantics.raw7871step1 line 477
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7871 line 479