OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical127.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4064 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw4064step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw4064step1 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw4064step2 line 20
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4064 line 22
  6. def OAI.MUB6.Certificate.PairSemantics.raw4065 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw4065step0 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw4065step1 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4065 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw4066 line 60
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4066 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw4067 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical4067 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw4068 line 72
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical4068 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw4069 line 78
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4069 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw4070 line 84
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4070 line 86
  20. def OAI.MUB6.Certificate.PairSemantics.raw4071 line 90
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4071 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw4072 line 96
  23. def OAI.MUB6.Certificate.PairSemantics.raw4072step0 line 98
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4072 line 100
  25. def OAI.MUB6.Certificate.PairSemantics.raw4073 line 109
  26. def OAI.MUB6.Certificate.PairSemantics.raw4073step0 line 111
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4073 line 113
  28. def OAI.MUB6.Certificate.PairSemantics.raw4074 line 122
  29. def OAI.MUB6.Certificate.PairSemantics.raw4074step0 line 124
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4074 line 126
  31. def OAI.MUB6.Certificate.PairSemantics.raw4075 line 135
  32. def OAI.MUB6.Certificate.PairSemantics.raw4075step0 line 137
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4075 line 139
  34. def OAI.MUB6.Certificate.PairSemantics.raw4076 line 148
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical4076 line 150
  36. def OAI.MUB6.Certificate.PairSemantics.raw4077 line 154
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4077 line 156
  38. def OAI.MUB6.Certificate.PairSemantics.raw4078 line 160
  39. def OAI.MUB6.Certificate.PairSemantics.raw4078step0 line 162
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4078 line 164
  41. def OAI.MUB6.Certificate.PairSemantics.raw4079 line 173
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4079 line 175
  43. def OAI.MUB6.Certificate.PairSemantics.raw4080 line 179
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4080 line 181
  45. def OAI.MUB6.Certificate.PairSemantics.raw4081 line 185
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical4081 line 187
  47. def OAI.MUB6.Certificate.PairSemantics.raw4082 line 191
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical4082 line 193
  49. def OAI.MUB6.Certificate.PairSemantics.raw4083 line 197
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical4083 line 199
  51. def OAI.MUB6.Certificate.PairSemantics.raw4084 line 203
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4084 line 205
  53. def OAI.MUB6.Certificate.PairSemantics.raw4085 line 209
  54. def OAI.MUB6.Certificate.PairSemantics.raw4085step0 line 211
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical4085 line 213
  56. def OAI.MUB6.Certificate.PairSemantics.raw4086 line 222
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4086 line 224
  58. def OAI.MUB6.Certificate.PairSemantics.raw4087 line 228
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4087 line 230
  60. def OAI.MUB6.Certificate.PairSemantics.raw4088 line 234
  61. def OAI.MUB6.Certificate.PairSemantics.raw4088step0 line 236
  62. def OAI.MUB6.Certificate.PairSemantics.raw4088step1 line 238
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical4088 line 240
  64. def OAI.MUB6.Certificate.PairSemantics.raw4089 line 253
  65. def OAI.MUB6.Certificate.PairSemantics.raw4089step0 line 255
  66. def OAI.MUB6.Certificate.PairSemantics.raw4089step1 line 257
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4089 line 259
  68. def OAI.MUB6.Certificate.PairSemantics.raw4090 line 272
  69. def OAI.MUB6.Certificate.PairSemantics.raw4090step0 line 274
  70. def OAI.MUB6.Certificate.PairSemantics.raw4090step1 line 276
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4090 line 278
  72. def OAI.MUB6.Certificate.PairSemantics.raw4091 line 291
  73. def OAI.MUB6.Certificate.PairSemantics.raw4091step0 line 293
  74. def OAI.MUB6.Certificate.PairSemantics.raw4091step1 line 295
  75. def OAI.MUB6.Certificate.PairSemantics.raw4091step2 line 297
  76. def OAI.MUB6.Certificate.PairSemantics.raw4091step3 line 299
  77. def OAI.MUB6.Certificate.PairSemantics.raw4091step4 line 301
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical4091 line 303
  79. def OAI.MUB6.Certificate.PairSemantics.raw4092 line 333
  80. def OAI.MUB6.Certificate.PairSemantics.raw4092step0 line 335
  81. def OAI.MUB6.Certificate.PairSemantics.raw4092step1 line 337
  82. def OAI.MUB6.Certificate.PairSemantics.raw4092step2 line 339
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical4092 line 341
  84. def OAI.MUB6.Certificate.PairSemantics.raw4093 line 361
  85. def OAI.MUB6.Certificate.PairSemantics.raw4093step0 line 363
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4093 line 365
  87. def OAI.MUB6.Certificate.PairSemantics.raw4094 line 375
  88. def OAI.MUB6.Certificate.PairSemantics.raw4094step0 line 377
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical4094 line 379
  90. def OAI.MUB6.Certificate.PairSemantics.raw4095 line 389
  91. def OAI.MUB6.Certificate.PairSemantics.raw4095step0 line 391
  92. def OAI.MUB6.Certificate.PairSemantics.raw4095step1 line 393
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical4095 line 395