OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical134.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4288 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw4288step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw4288step1 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw4288step2 line 23
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4288 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw4289 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw4289step0 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw4289step1 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4289 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw4290 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw4290step0 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw4290step1 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw4290step2 line 67
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4290 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw4291 line 86
  16. def OAI.MUB6.Certificate.PairSemantics.raw4291step0 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw4291step1 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw4291step2 line 92
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4291 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw4292 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw4292step0 line 113
  22. def OAI.MUB6.Certificate.PairSemantics.raw4292step1 line 115
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4292 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw4293 line 130
  25. def OAI.MUB6.Certificate.PairSemantics.raw4293step0 line 132
  26. def OAI.MUB6.Certificate.PairSemantics.raw4293step1 line 134
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical4293 line 136
  28. def OAI.MUB6.Certificate.PairSemantics.raw4294 line 149
  29. def OAI.MUB6.Certificate.PairSemantics.raw4294step0 line 151
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4294 line 153
  31. def OAI.MUB6.Certificate.PairSemantics.raw4295 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw4295step0 line 164
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical4295 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw4296 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw4296step0 line 177
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4296 line 179
  37. def OAI.MUB6.Certificate.PairSemantics.raw4297 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw4297step0 line 190
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical4297 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw4298 line 201
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical4298 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw4299 line 207
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical4299 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw4300 line 213
  45. def OAI.MUB6.Certificate.PairSemantics.raw4300step0 line 215
  46. def OAI.MUB6.Certificate.PairSemantics.raw4300step1 line 217
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4300 line 219
  48. def OAI.MUB6.Certificate.PairSemantics.raw4301 line 232
  49. def OAI.MUB6.Certificate.PairSemantics.raw4301step0 line 234
  50. def OAI.MUB6.Certificate.PairSemantics.raw4301step1 line 236
  51. def OAI.MUB6.Certificate.PairSemantics.raw4301step2 line 238
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical4301 line 240
  53. def OAI.MUB6.Certificate.PairSemantics.raw4302 line 257
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4302 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw4303 line 263
  56. def OAI.MUB6.Certificate.PairSemantics.raw4303step0 line 265
  57. def OAI.MUB6.Certificate.PairSemantics.raw4303step1 line 267
  58. def OAI.MUB6.Certificate.PairSemantics.raw4303step2 line 269
  59. def OAI.MUB6.Certificate.PairSemantics.raw4303step3 line 271
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical4303 line 273
  61. def OAI.MUB6.Certificate.PairSemantics.raw4304 line 295
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical4304 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw4305 line 301
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical4305 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw4306 line 307
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4306 line 309
  67. def OAI.MUB6.Certificate.PairSemantics.raw4307 line 313
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical4307 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw4308 line 319
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical4308 line 321
  71. def OAI.MUB6.Certificate.PairSemantics.raw4309 line 325
  72. def OAI.MUB6.Certificate.PairSemantics.raw4309step0 line 327
  73. def OAI.MUB6.Certificate.PairSemantics.raw4309step1 line 329
  74. def OAI.MUB6.Certificate.PairSemantics.raw4309step2 line 331
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4309 line 333
  76. def OAI.MUB6.Certificate.PairSemantics.raw4310 line 350
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical4310 line 352
  78. def OAI.MUB6.Certificate.PairSemantics.raw4311 line 356
  79. def OAI.MUB6.Certificate.PairSemantics.raw4311step0 line 358
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical4311 line 360
  81. def OAI.MUB6.Certificate.PairSemantics.raw4312 line 369
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4312 line 371
  83. def OAI.MUB6.Certificate.PairSemantics.raw4313 line 375
  84. def OAI.MUB6.Certificate.PairSemantics.raw4313step0 line 377
  85. def OAI.MUB6.Certificate.PairSemantics.raw4313step1 line 379
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical4313 line 381
  87. def OAI.MUB6.Certificate.PairSemantics.raw4314 line 394
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical4314 line 396
  89. def OAI.MUB6.Certificate.PairSemantics.raw4315 line 400
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4315 line 402
  91. def OAI.MUB6.Certificate.PairSemantics.raw4316 line 406
  92. def OAI.MUB6.Certificate.PairSemantics.raw4316step0 line 408
  93. def OAI.MUB6.Certificate.PairSemantics.raw4316step1 line 410
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical4316 line 412
  95. def OAI.MUB6.Certificate.PairSemantics.raw4317 line 425
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical4317 line 427
  97. def OAI.MUB6.Certificate.PairSemantics.raw4318 line 431
  98. def OAI.MUB6.Certificate.PairSemantics.raw4318step0 line 433
  99. def OAI.MUB6.Certificate.PairSemantics.raw4318step1 line 435
  100. def OAI.MUB6.Certificate.PairSemantics.raw4318step2 line 437
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical4318 line 439
  102. def OAI.MUB6.Certificate.PairSemantics.raw4319 line 456
  103. def OAI.MUB6.Certificate.PairSemantics.raw4319step0 line 458
  104. def OAI.MUB6.Certificate.PairSemantics.raw4319step1 line 460
  105. def OAI.MUB6.Certificate.PairSemantics.raw4319step2 line 462
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical4319 line 464