OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical89.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2848 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2848 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw2849 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2849 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw2850 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2850 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw2851 line 31
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2851 line 33
  9. def OAI.MUB6.Certificate.PairSemantics.raw2852 line 37
  10. def OAI.MUB6.Certificate.PairSemantics.raw2852step0 line 39
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2852 line 41
  12. def OAI.MUB6.Certificate.PairSemantics.raw2853 line 50
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2853 line 52
  14. def OAI.MUB6.Certificate.PairSemantics.raw2854 line 56
  15. def OAI.MUB6.Certificate.PairSemantics.raw2854step0 line 58
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2854 line 60
  17. def OAI.MUB6.Certificate.PairSemantics.raw2855 line 69
  18. def OAI.MUB6.Certificate.PairSemantics.raw2855step0 line 71
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2855 line 73
  20. def OAI.MUB6.Certificate.PairSemantics.raw2856 line 82
  21. def OAI.MUB6.Certificate.PairSemantics.raw2856step0 line 84
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2856 line 86
  23. def OAI.MUB6.Certificate.PairSemantics.raw2857 line 95
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2857 line 97
  25. def OAI.MUB6.Certificate.PairSemantics.raw2858 line 101
  26. def OAI.MUB6.Certificate.PairSemantics.raw2858step0 line 103
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2858 line 105
  28. def OAI.MUB6.Certificate.PairSemantics.raw2859 line 114
  29. def OAI.MUB6.Certificate.PairSemantics.raw2859step0 line 116
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2859 line 118
  31. def OAI.MUB6.Certificate.PairSemantics.raw2860 line 127
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2860 line 129
  33. def OAI.MUB6.Certificate.PairSemantics.raw2861 line 133
  34. def OAI.MUB6.Certificate.PairSemantics.raw2861step0 line 135
  35. def OAI.MUB6.Certificate.PairSemantics.raw2861step1 line 137
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2861 line 139
  37. def OAI.MUB6.Certificate.PairSemantics.raw2862 line 152
  38. def OAI.MUB6.Certificate.PairSemantics.raw2862step0 line 154
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2862 line 156
  40. def OAI.MUB6.Certificate.PairSemantics.raw2863 line 165
  41. def OAI.MUB6.Certificate.PairSemantics.raw2863step0 line 167
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2863 line 169
  43. def OAI.MUB6.Certificate.PairSemantics.raw2864 line 178
  44. def OAI.MUB6.Certificate.PairSemantics.raw2864step0 line 180
  45. def OAI.MUB6.Certificate.PairSemantics.raw2864step1 line 182
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2864 line 184
  47. def OAI.MUB6.Certificate.PairSemantics.raw2865 line 197
  48. def OAI.MUB6.Certificate.PairSemantics.raw2865step0 line 199
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2865 line 201
  50. def OAI.MUB6.Certificate.PairSemantics.raw2866 line 210
  51. def OAI.MUB6.Certificate.PairSemantics.raw2866step0 line 212
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2866 line 214
  53. def OAI.MUB6.Certificate.PairSemantics.raw2867 line 223
  54. def OAI.MUB6.Certificate.PairSemantics.raw2867step0 line 225
  55. def OAI.MUB6.Certificate.PairSemantics.raw2867step1 line 227
  56. def OAI.MUB6.Certificate.PairSemantics.raw2867step2 line 229
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2867 line 231
  58. def OAI.MUB6.Certificate.PairSemantics.raw2868 line 248
  59. def OAI.MUB6.Certificate.PairSemantics.raw2868step0 line 250
  60. def OAI.MUB6.Certificate.PairSemantics.raw2868step1 line 252
  61. def OAI.MUB6.Certificate.PairSemantics.raw2868step2 line 254
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2868 line 256
  63. def OAI.MUB6.Certificate.PairSemantics.raw2869 line 273
  64. def OAI.MUB6.Certificate.PairSemantics.raw2869step0 line 275
  65. def OAI.MUB6.Certificate.PairSemantics.raw2869step1 line 277
  66. def OAI.MUB6.Certificate.PairSemantics.raw2869step2 line 279
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2869 line 281
  68. def OAI.MUB6.Certificate.PairSemantics.raw2870 line 298
  69. def OAI.MUB6.Certificate.PairSemantics.raw2870step0 line 300
  70. def OAI.MUB6.Certificate.PairSemantics.raw2870step1 line 302
  71. def OAI.MUB6.Certificate.PairSemantics.raw2870step2 line 304
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2870 line 306
  73. def OAI.MUB6.Certificate.PairSemantics.raw2871 line 323
  74. def OAI.MUB6.Certificate.PairSemantics.raw2871step0 line 325
  75. def OAI.MUB6.Certificate.PairSemantics.raw2871step1 line 327
  76. def OAI.MUB6.Certificate.PairSemantics.raw2871step2 line 329
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2871 line 331
  78. def OAI.MUB6.Certificate.PairSemantics.raw2872 line 348
  79. def OAI.MUB6.Certificate.PairSemantics.raw2872step0 line 350
  80. def OAI.MUB6.Certificate.PairSemantics.raw2872step1 line 352
  81. def OAI.MUB6.Certificate.PairSemantics.raw2872step2 line 354
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2872 line 356
  83. def OAI.MUB6.Certificate.PairSemantics.raw2873 line 373
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2873 line 375
  85. def OAI.MUB6.Certificate.PairSemantics.raw2874 line 379
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2874 line 381
  87. def OAI.MUB6.Certificate.PairSemantics.raw2875 line 385
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2875 line 387
  89. def OAI.MUB6.Certificate.PairSemantics.raw2876 line 391
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2876 line 393
  91. def OAI.MUB6.Certificate.PairSemantics.raw2877 line 397
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2877 line 399
  93. def OAI.MUB6.Certificate.PairSemantics.raw2878 line 403
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2878 line 405
  95. def OAI.MUB6.Certificate.PairSemantics.raw2879 line 409
  96. def OAI.MUB6.Certificate.PairSemantics.raw2879step0 line 411
  97. def OAI.MUB6.Certificate.PairSemantics.raw2879step1 line 413
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2879 line 415