OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical185.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5920 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw5920step0 line 13
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical5920 line 15
  4. def OAI.MUB6.Certificate.PairSemantics.raw5921 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw5921step0 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5921 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw5922 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw5922step0 line 39
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical5922 line 41
  10. def OAI.MUB6.Certificate.PairSemantics.raw5923 line 50
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical5923 line 52
  12. def OAI.MUB6.Certificate.PairSemantics.raw5924 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw5924step0 line 58
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5924 line 60
  15. def OAI.MUB6.Certificate.PairSemantics.raw5925 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw5925step0 line 72
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical5925 line 74
  18. def OAI.MUB6.Certificate.PairSemantics.raw5926 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw5926step0 line 86
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5926 line 88
  21. def OAI.MUB6.Certificate.PairSemantics.raw5927 line 98
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical5927 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw5928 line 104
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5928 line 106
  25. def OAI.MUB6.Certificate.PairSemantics.raw5929 line 110
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5929 line 112
  27. def OAI.MUB6.Certificate.PairSemantics.raw5930 line 116
  28. def OAI.MUB6.Certificate.PairSemantics.raw5930step0 line 118
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5930 line 120
  30. def OAI.MUB6.Certificate.PairSemantics.raw5931 line 129
  31. def OAI.MUB6.Certificate.PairSemantics.raw5931step0 line 131
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5931 line 133
  33. def OAI.MUB6.Certificate.PairSemantics.raw5932 line 142
  34. def OAI.MUB6.Certificate.PairSemantics.raw5932step0 line 144
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5932 line 146
  36. def OAI.MUB6.Certificate.PairSemantics.raw5933 line 155
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical5933 line 157
  38. def OAI.MUB6.Certificate.PairSemantics.raw5934 line 161
  39. def OAI.MUB6.Certificate.PairSemantics.raw5934step0 line 163
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical5934 line 165
  41. def OAI.MUB6.Certificate.PairSemantics.raw5935 line 175
  42. def OAI.MUB6.Certificate.PairSemantics.raw5935step0 line 177
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5935 line 179
  44. def OAI.MUB6.Certificate.PairSemantics.raw5936 line 188
  45. def OAI.MUB6.Certificate.PairSemantics.raw5936step0 line 190
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5936 line 192
  47. def OAI.MUB6.Certificate.PairSemantics.raw5937 line 201
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical5937 line 203
  49. def OAI.MUB6.Certificate.PairSemantics.raw5938 line 207
  50. def OAI.MUB6.Certificate.PairSemantics.raw5938step0 line 209
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5938 line 211
  52. def OAI.MUB6.Certificate.PairSemantics.raw5939 line 221
  53. def OAI.MUB6.Certificate.PairSemantics.raw5939step0 line 223
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5939 line 225
  55. def OAI.MUB6.Certificate.PairSemantics.raw5940 line 234
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5940 line 236
  57. def OAI.MUB6.Certificate.PairSemantics.raw5941 line 240
  58. def OAI.MUB6.Certificate.PairSemantics.raw5941step0 line 242
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical5941 line 244
  60. def OAI.MUB6.Certificate.PairSemantics.raw5942 line 254
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical5942 line 256
  62. def OAI.MUB6.Certificate.PairSemantics.raw5943 line 260
  63. def OAI.MUB6.Certificate.PairSemantics.raw5943step0 line 262
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical5943 line 264
  65. def OAI.MUB6.Certificate.PairSemantics.raw5944 line 273
  66. def OAI.MUB6.Certificate.PairSemantics.raw5944step0 line 275
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical5944 line 277
  68. def OAI.MUB6.Certificate.PairSemantics.raw5945 line 287
  69. def OAI.MUB6.Certificate.PairSemantics.raw5945step0 line 289
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical5945 line 291
  71. def OAI.MUB6.Certificate.PairSemantics.raw5946 line 301
  72. def OAI.MUB6.Certificate.PairSemantics.raw5946step0 line 303
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical5946 line 305
  74. def OAI.MUB6.Certificate.PairSemantics.raw5947 line 315
  75. def OAI.MUB6.Certificate.PairSemantics.raw5947step0 line 317
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5947 line 319
  77. def OAI.MUB6.Certificate.PairSemantics.raw5948 line 329
  78. def OAI.MUB6.Certificate.PairSemantics.raw5948step0 line 331
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5948 line 333
  80. def OAI.MUB6.Certificate.PairSemantics.raw5949 line 343
  81. def OAI.MUB6.Certificate.PairSemantics.raw5949step0 line 345
  82. def OAI.MUB6.Certificate.PairSemantics.raw5949step1 line 347
  83. def OAI.MUB6.Certificate.PairSemantics.raw5949step2 line 349
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5949 line 351
  85. def OAI.MUB6.Certificate.PairSemantics.raw5950 line 369
  86. def OAI.MUB6.Certificate.PairSemantics.raw5950step0 line 371
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical5950 line 373
  88. def OAI.MUB6.Certificate.PairSemantics.raw5951 line 382
  89. def OAI.MUB6.Certificate.PairSemantics.raw5951step0 line 384
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical5951 line 386