OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical189.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6048 line 14
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical6048 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw6049 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6049 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw6050 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6050 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw6051 line 32
  8. def OAI.MUB6.Certificate.PairSemantics.raw6051step0 line 34
  9. def OAI.MUB6.Certificate.PairSemantics.raw6051step1 line 36
  10. def OAI.MUB6.Certificate.PairSemantics.raw6051step2 line 38
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6051 line 40
  12. def OAI.MUB6.Certificate.PairSemantics.raw6052 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw6052step0 line 59
  14. def OAI.MUB6.Certificate.PairSemantics.raw6052step1 line 61
  15. def OAI.MUB6.Certificate.PairSemantics.raw6052step2 line 63
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6052 line 65
  17. def OAI.MUB6.Certificate.PairSemantics.raw6053 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw6053step0 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6053 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw6054 line 96
  21. def OAI.MUB6.Certificate.PairSemantics.raw6054step0 line 98
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6054 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw6055 line 109
  24. def OAI.MUB6.Certificate.PairSemantics.raw6055step0 line 111
  25. def OAI.MUB6.Certificate.PairSemantics.raw6055step1 line 113
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6055 line 115
  27. def OAI.MUB6.Certificate.PairSemantics.raw6056 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw6056step0 line 130
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6056 line 132
  30. def OAI.MUB6.Certificate.PairSemantics.raw6057 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw6057step0 line 143
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6057 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw6058 line 154
  34. def OAI.MUB6.Certificate.PairSemantics.raw6058step0 line 156
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6058 line 158
  36. def OAI.MUB6.Certificate.PairSemantics.raw6059 line 167
  37. def OAI.MUB6.Certificate.PairSemantics.raw6059step0 line 169
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6059 line 171
  39. def OAI.MUB6.Certificate.PairSemantics.raw6060 line 181
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6060 line 183
  41. def OAI.MUB6.Certificate.PairSemantics.raw6061 line 187
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical6061 line 189
  43. def OAI.MUB6.Certificate.PairSemantics.raw6062 line 193
  44. def OAI.MUB6.Certificate.PairSemantics.raw6062step0 line 195
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6062 line 197
  46. def OAI.MUB6.Certificate.PairSemantics.raw6063 line 206
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6063 line 208
  48. def OAI.MUB6.Certificate.PairSemantics.raw6064 line 212
  49. def OAI.MUB6.Certificate.PairSemantics.raw6064step0 line 214
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6064 line 216
  51. def OAI.MUB6.Certificate.PairSemantics.raw6065 line 225
  52. def OAI.MUB6.Certificate.PairSemantics.raw6065step0 line 227
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical6065 line 229
  54. def OAI.MUB6.Certificate.PairSemantics.raw6066 line 238
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6066 line 240
  56. def OAI.MUB6.Certificate.PairSemantics.raw6067 line 244
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6067 line 246
  58. def OAI.MUB6.Certificate.PairSemantics.raw6068 line 250
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6068 line 252
  60. def OAI.MUB6.Certificate.PairSemantics.raw6069 line 256
  61. def OAI.MUB6.Certificate.PairSemantics.raw6069step0 line 258
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical6069 line 260
  63. def OAI.MUB6.Certificate.PairSemantics.raw6070 line 269
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6070 line 271
  65. def OAI.MUB6.Certificate.PairSemantics.raw6071 line 275
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6071 line 277
  67. def OAI.MUB6.Certificate.PairSemantics.raw6072 line 281
  68. def OAI.MUB6.Certificate.PairSemantics.raw6072step0 line 283
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6072 line 285
  70. def OAI.MUB6.Certificate.PairSemantics.raw6073 line 294
  71. def OAI.MUB6.Certificate.PairSemantics.raw6073step0 line 296
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6073 line 298
  73. def OAI.MUB6.Certificate.PairSemantics.raw6074 line 307
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6074 line 309
  75. def OAI.MUB6.Certificate.PairSemantics.raw6075 line 313
  76. def OAI.MUB6.Certificate.PairSemantics.raw6075step0 line 315
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6075 line 317
  78. def OAI.MUB6.Certificate.PairSemantics.raw6076 line 326
  79. def OAI.MUB6.Certificate.PairSemantics.raw6076step0 line 328
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical6076 line 330
  81. def OAI.MUB6.Certificate.PairSemantics.raw6077 line 339
  82. def OAI.MUB6.Certificate.PairSemantics.raw6077step0 line 341
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6077 line 343
  84. def OAI.MUB6.Certificate.PairSemantics.raw6078 line 352
  85. def OAI.MUB6.Certificate.PairSemantics.raw6078step0 line 354
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6078 line 356
  87. def OAI.MUB6.Certificate.PairSemantics.raw6079 line 365
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6079 line 367