OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical184.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5888 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5888 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw5889 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw5889step0 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5889 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw5890 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw5890step0 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5890 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw5891 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw5891step0 line 47
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5891 line 49
  12. def OAI.MUB6.Certificate.PairSemantics.raw5892 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical5892 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw5893 line 64
  15. def OAI.MUB6.Certificate.PairSemantics.raw5893step0 line 66
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5893 line 68
  17. def OAI.MUB6.Certificate.PairSemantics.raw5894 line 77
  18. def OAI.MUB6.Certificate.PairSemantics.raw5894step0 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw5894step1 line 81
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5894 line 83
  21. def OAI.MUB6.Certificate.PairSemantics.raw5895 line 96
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5895 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw5896 line 102
  24. def OAI.MUB6.Certificate.PairSemantics.raw5896step0 line 104
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5896 line 106
  26. def OAI.MUB6.Certificate.PairSemantics.raw5897 line 116
  27. def OAI.MUB6.Certificate.PairSemantics.raw5897step0 line 118
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical5897 line 120
  29. def OAI.MUB6.Certificate.PairSemantics.raw5898 line 129
  30. def OAI.MUB6.Certificate.PairSemantics.raw5898step0 line 131
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical5898 line 133
  32. def OAI.MUB6.Certificate.PairSemantics.raw5899 line 142
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5899 line 144
  34. def OAI.MUB6.Certificate.PairSemantics.raw5900 line 148
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5900 line 150
  36. def OAI.MUB6.Certificate.PairSemantics.raw5901 line 154
  37. def OAI.MUB6.Certificate.PairSemantics.raw5901step0 line 156
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5901 line 158
  39. def OAI.MUB6.Certificate.PairSemantics.raw5902 line 167
  40. def OAI.MUB6.Certificate.PairSemantics.raw5902step0 line 169
  41. def OAI.MUB6.Certificate.PairSemantics.raw5902step1 line 171
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical5902 line 173
  43. def OAI.MUB6.Certificate.PairSemantics.raw5903 line 186
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical5903 line 188
  45. def OAI.MUB6.Certificate.PairSemantics.raw5904 line 192
  46. def OAI.MUB6.Certificate.PairSemantics.raw5904step0 line 194
  47. def OAI.MUB6.Certificate.PairSemantics.raw5904step1 line 196
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5904 line 198
  49. def OAI.MUB6.Certificate.PairSemantics.raw5905 line 211
  50. def OAI.MUB6.Certificate.PairSemantics.raw5905step0 line 213
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5905 line 215
  52. def OAI.MUB6.Certificate.PairSemantics.raw5906 line 224
  53. def OAI.MUB6.Certificate.PairSemantics.raw5906step0 line 226
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5906 line 228
  55. def OAI.MUB6.Certificate.PairSemantics.raw5907 line 237
  56. def OAI.MUB6.Certificate.PairSemantics.raw5907step0 line 239
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical5907 line 241
  58. def OAI.MUB6.Certificate.PairSemantics.raw5908 line 250
  59. def OAI.MUB6.Certificate.PairSemantics.raw5908step0 line 252
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5908 line 254
  61. def OAI.MUB6.Certificate.PairSemantics.raw5909 line 263
  62. def OAI.MUB6.Certificate.PairSemantics.raw5909step0 line 265
  63. def OAI.MUB6.Certificate.PairSemantics.raw5909step1 line 267
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5909 line 269
  65. def OAI.MUB6.Certificate.PairSemantics.raw5910 line 282
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5910 line 284
  67. def OAI.MUB6.Certificate.PairSemantics.raw5911 line 288
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5911 line 290
  69. def OAI.MUB6.Certificate.PairSemantics.raw5912 line 294
  70. def OAI.MUB6.Certificate.PairSemantics.raw5912step0 line 296
  71. def OAI.MUB6.Certificate.PairSemantics.raw5912step1 line 298
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5912 line 300
  73. def OAI.MUB6.Certificate.PairSemantics.raw5913 line 313
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5913 line 315
  75. def OAI.MUB6.Certificate.PairSemantics.raw5914 line 319
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5914 line 321
  77. def OAI.MUB6.Certificate.PairSemantics.raw5915 line 325
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical5915 line 327
  79. def OAI.MUB6.Certificate.PairSemantics.raw5916 line 331
  80. def OAI.MUB6.Certificate.PairSemantics.raw5916step0 line 333
  81. def OAI.MUB6.Certificate.PairSemantics.raw5916step1 line 335
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical5916 line 337
  83. def OAI.MUB6.Certificate.PairSemantics.raw5917 line 350
  84. def OAI.MUB6.Certificate.PairSemantics.raw5917step0 line 352
  85. def OAI.MUB6.Certificate.PairSemantics.raw5917step1 line 354
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical5917 line 356
  87. def OAI.MUB6.Certificate.PairSemantics.raw5918 line 369
  88. def OAI.MUB6.Certificate.PairSemantics.raw5918step0 line 371
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical5918 line 373
  90. def OAI.MUB6.Certificate.PairSemantics.raw5919 line 382
  91. def OAI.MUB6.Certificate.PairSemantics.raw5919step0 line 384
  92. def OAI.MUB6.Certificate.PairSemantics.raw5919step1 line 386
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical5919 line 388