OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical88.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2816 line 11
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2816 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw2817 line 17
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2817 line 19
  5. def OAI.MUB6.Certificate.PairSemantics.raw2818 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw2818step0 line 25
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2818 line 27
  8. def OAI.MUB6.Certificate.PairSemantics.raw2819 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw2819step0 line 38
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical2819 line 40
  11. def OAI.MUB6.Certificate.PairSemantics.raw2820 line 49
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2820 line 51
  13. def OAI.MUB6.Certificate.PairSemantics.raw2821 line 55
  14. def OAI.MUB6.Certificate.PairSemantics.raw2821step0 line 57
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2821 line 59
  16. def OAI.MUB6.Certificate.PairSemantics.raw2822 line 68
  17. def OAI.MUB6.Certificate.PairSemantics.raw2822step0 line 70
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2822 line 72
  19. def OAI.MUB6.Certificate.PairSemantics.raw2823 line 81
  20. def OAI.MUB6.Certificate.PairSemantics.raw2823step0 line 83
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2823 line 85
  22. def OAI.MUB6.Certificate.PairSemantics.raw2824 line 94
  23. def OAI.MUB6.Certificate.PairSemantics.raw2824step0 line 96
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2824 line 98
  25. def OAI.MUB6.Certificate.PairSemantics.raw2825 line 107
  26. def OAI.MUB6.Certificate.PairSemantics.raw2825step0 line 109
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2825 line 111
  28. def OAI.MUB6.Certificate.PairSemantics.raw2826 line 120
  29. def OAI.MUB6.Certificate.PairSemantics.raw2826step0 line 122
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2826 line 124
  31. def OAI.MUB6.Certificate.PairSemantics.raw2827 line 133
  32. def OAI.MUB6.Certificate.PairSemantics.raw2827step0 line 135
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2827 line 137
  34. def OAI.MUB6.Certificate.PairSemantics.raw2828 line 146
  35. def OAI.MUB6.Certificate.PairSemantics.raw2828step0 line 148
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2828 line 150
  37. def OAI.MUB6.Certificate.PairSemantics.raw2829 line 159
  38. def OAI.MUB6.Certificate.PairSemantics.raw2829step0 line 161
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2829 line 163
  40. def OAI.MUB6.Certificate.PairSemantics.raw2830 line 172
  41. def OAI.MUB6.Certificate.PairSemantics.raw2830step0 line 174
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2830 line 176
  43. def OAI.MUB6.Certificate.PairSemantics.raw2831 line 185
  44. def OAI.MUB6.Certificate.PairSemantics.raw2831step0 line 187
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2831 line 189
  46. def OAI.MUB6.Certificate.PairSemantics.raw2832 line 198
  47. def OAI.MUB6.Certificate.PairSemantics.raw2832step0 line 200
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2832 line 202
  49. def OAI.MUB6.Certificate.PairSemantics.raw2833 line 211
  50. def OAI.MUB6.Certificate.PairSemantics.raw2833step0 line 213
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2833 line 215
  52. def OAI.MUB6.Certificate.PairSemantics.raw2834 line 224
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2834 line 226
  54. def OAI.MUB6.Certificate.PairSemantics.raw2835 line 230
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2835 line 232
  56. def OAI.MUB6.Certificate.PairSemantics.raw2836 line 236
  57. def OAI.MUB6.Certificate.PairSemantics.raw2836step0 line 238
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical2836 line 240
  59. def OAI.MUB6.Certificate.PairSemantics.raw2837 line 250
  60. def OAI.MUB6.Certificate.PairSemantics.raw2837step0 line 252
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2837 line 254
  62. def OAI.MUB6.Certificate.PairSemantics.raw2838 line 263
  63. def OAI.MUB6.Certificate.PairSemantics.raw2838step0 line 265
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2838 line 267
  65. def OAI.MUB6.Certificate.PairSemantics.raw2839 line 276
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2839 line 278
  67. def OAI.MUB6.Certificate.PairSemantics.raw2840 line 282
  68. def OAI.MUB6.Certificate.PairSemantics.raw2840step0 line 284
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2840 line 286
  70. def OAI.MUB6.Certificate.PairSemantics.raw2841 line 295
  71. def OAI.MUB6.Certificate.PairSemantics.raw2841step0 line 297
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2841 line 299
  73. def OAI.MUB6.Certificate.PairSemantics.raw2842 line 308
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical2842 line 310
  75. def OAI.MUB6.Certificate.PairSemantics.raw2843 line 314
  76. def OAI.MUB6.Certificate.PairSemantics.raw2843step0 line 316
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2843 line 318
  78. def OAI.MUB6.Certificate.PairSemantics.raw2844 line 327
  79. def OAI.MUB6.Certificate.PairSemantics.raw2844step0 line 329
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2844 line 331
  81. def OAI.MUB6.Certificate.PairSemantics.raw2845 line 340
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2845 line 342
  83. def OAI.MUB6.Certificate.PairSemantics.raw2846 line 346
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2846 line 348
  85. def OAI.MUB6.Certificate.PairSemantics.raw2847 line 352
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2847 line 354