OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical183.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5856 line 14
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical5856 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw5857 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw5857step0 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw5857step1 line 24
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical5857 line 26
  7. def OAI.MUB6.Certificate.PairSemantics.raw5858 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical5858 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw5859 line 45
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical5859 line 47
  11. def OAI.MUB6.Certificate.PairSemantics.raw5860 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw5860step0 line 53
  13. def OAI.MUB6.Certificate.PairSemantics.raw5860step1 line 55
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical5860 line 57
  15. def OAI.MUB6.Certificate.PairSemantics.raw5861 line 70
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical5861 line 72
  17. def OAI.MUB6.Certificate.PairSemantics.raw5862 line 76
  18. def OAI.MUB6.Certificate.PairSemantics.raw5862step0 line 78
  19. def OAI.MUB6.Certificate.PairSemantics.raw5862step1 line 80
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5862 line 82
  21. def OAI.MUB6.Certificate.PairSemantics.raw5863 line 95
  22. def OAI.MUB6.Certificate.PairSemantics.raw5863step0 line 97
  23. def OAI.MUB6.Certificate.PairSemantics.raw5863step1 line 99
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical5863 line 101
  25. def OAI.MUB6.Certificate.PairSemantics.raw5864 line 114
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical5864 line 116
  27. def OAI.MUB6.Certificate.PairSemantics.raw5865 line 120
  28. def OAI.MUB6.Certificate.PairSemantics.raw5865step0 line 122
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical5865 line 124
  30. def OAI.MUB6.Certificate.PairSemantics.raw5866 line 133
  31. def OAI.MUB6.Certificate.PairSemantics.raw5866step0 line 135
  32. def OAI.MUB6.Certificate.PairSemantics.raw5866step1 line 137
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical5866 line 139
  34. def OAI.MUB6.Certificate.PairSemantics.raw5867 line 152
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical5867 line 154
  36. def OAI.MUB6.Certificate.PairSemantics.raw5868 line 158
  37. def OAI.MUB6.Certificate.PairSemantics.raw5868step0 line 160
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical5868 line 162
  39. def OAI.MUB6.Certificate.PairSemantics.raw5869 line 171
  40. def OAI.MUB6.Certificate.PairSemantics.raw5869step0 line 173
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5869 line 175
  42. def OAI.MUB6.Certificate.PairSemantics.raw5870 line 184
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5870 line 186
  44. def OAI.MUB6.Certificate.PairSemantics.raw5871 line 190
  45. def OAI.MUB6.Certificate.PairSemantics.raw5871step0 line 192
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5871 line 194
  47. def OAI.MUB6.Certificate.PairSemantics.raw5872 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw5872step0 line 205
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical5872 line 207
  50. def OAI.MUB6.Certificate.PairSemantics.raw5873 line 216
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical5873 line 218
  52. def OAI.MUB6.Certificate.PairSemantics.raw5874 line 222
  53. def OAI.MUB6.Certificate.PairSemantics.raw5874step0 line 224
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5874 line 226
  55. def OAI.MUB6.Certificate.PairSemantics.raw5875 line 235
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical5875 line 237
  57. def OAI.MUB6.Certificate.PairSemantics.raw5876 line 241
  58. def OAI.MUB6.Certificate.PairSemantics.raw5876step0 line 243
  59. def OAI.MUB6.Certificate.PairSemantics.raw5876step1 line 245
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical5876 line 247
  61. def OAI.MUB6.Certificate.PairSemantics.raw5877 line 260
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5877 line 262
  63. def OAI.MUB6.Certificate.PairSemantics.raw5878 line 266
  64. def OAI.MUB6.Certificate.PairSemantics.raw5878step0 line 268
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical5878 line 270
  66. def OAI.MUB6.Certificate.PairSemantics.raw5879 line 279
  67. def OAI.MUB6.Certificate.PairSemantics.raw5879step0 line 281
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical5879 line 283
  69. def OAI.MUB6.Certificate.PairSemantics.raw5880 line 293
  70. def OAI.MUB6.Certificate.PairSemantics.raw5880step0 line 295
  71. def OAI.MUB6.Certificate.PairSemantics.raw5880step1 line 297
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical5880 line 299
  73. def OAI.MUB6.Certificate.PairSemantics.raw5881 line 313
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical5881 line 315
  75. def OAI.MUB6.Certificate.PairSemantics.raw5882 line 319
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical5882 line 321
  77. def OAI.MUB6.Certificate.PairSemantics.raw5883 line 325
  78. def OAI.MUB6.Certificate.PairSemantics.raw5883step0 line 327
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5883 line 329
  80. def OAI.MUB6.Certificate.PairSemantics.raw5884 line 338
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical5884 line 340
  82. def OAI.MUB6.Certificate.PairSemantics.raw5885 line 344
  83. def OAI.MUB6.Certificate.PairSemantics.raw5885step0 line 346
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5885 line 348
  85. def OAI.MUB6.Certificate.PairSemantics.raw5886 line 357
  86. def OAI.MUB6.Certificate.PairSemantics.raw5886step0 line 359
  87. def OAI.MUB6.Certificate.PairSemantics.raw5886step1 line 361
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5886 line 363
  89. def OAI.MUB6.Certificate.PairSemantics.raw5887 line 376
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical5887 line 378