OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical201.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6432 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw6432step0 line 19
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6432 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw6433 line 30
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6433 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw6434 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw6434step0 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw6434step1 line 40
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6434 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw6435 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6435 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw6436 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical6436 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw6437 line 67
  15. def OAI.MUB6.Certificate.PairSemantics.raw6437step0 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw6437step1 line 71
  17. def OAI.MUB6.Certificate.PairSemantics.raw6437step2 line 73
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6437 line 75
  19. def OAI.MUB6.Certificate.PairSemantics.raw6438 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw6438step0 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw6438step1 line 96
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6438 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw6439 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw6439step0 line 113
  25. def OAI.MUB6.Certificate.PairSemantics.raw6439step1 line 115
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical6439 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw6440 line 130
  28. def OAI.MUB6.Certificate.PairSemantics.raw6440step0 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw6440step1 line 134
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical6440 line 136
  31. def OAI.MUB6.Certificate.PairSemantics.raw6441 line 149
  32. def OAI.MUB6.Certificate.PairSemantics.raw6441step0 line 151
  33. def OAI.MUB6.Certificate.PairSemantics.raw6441step1 line 153
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6441 line 155
  35. def OAI.MUB6.Certificate.PairSemantics.raw6442 line 168
  36. def OAI.MUB6.Certificate.PairSemantics.raw6442step0 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw6442step1 line 172
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6442 line 174
  39. def OAI.MUB6.Certificate.PairSemantics.raw6443 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6443 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw6444 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw6444step0 line 195
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6444 line 197
  44. def OAI.MUB6.Certificate.PairSemantics.raw6445 line 206
  45. def OAI.MUB6.Certificate.PairSemantics.raw6445step0 line 208
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6445 line 210
  47. def OAI.MUB6.Certificate.PairSemantics.raw6446 line 219
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6446 line 221
  49. def OAI.MUB6.Certificate.PairSemantics.raw6447 line 225
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6447 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw6448 line 231
  52. def OAI.MUB6.Certificate.PairSemantics.raw6448step0 line 233
  53. def OAI.MUB6.Certificate.PairSemantics.raw6448step1 line 235
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6448 line 237
  55. def OAI.MUB6.Certificate.PairSemantics.raw6449 line 250
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6449 line 252
  57. def OAI.MUB6.Certificate.PairSemantics.raw6450 line 256
  58. def OAI.MUB6.Certificate.PairSemantics.raw6450step0 line 258
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6450 line 260
  60. def OAI.MUB6.Certificate.PairSemantics.raw6451 line 269
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical6451 line 271
  62. def OAI.MUB6.Certificate.PairSemantics.raw6452 line 275
  63. def OAI.MUB6.Certificate.PairSemantics.raw6452step0 line 277
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6452 line 279
  65. def OAI.MUB6.Certificate.PairSemantics.raw6453 line 288
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6453 line 290
  67. def OAI.MUB6.Certificate.PairSemantics.raw6454 line 294
  68. def OAI.MUB6.Certificate.PairSemantics.raw6454step0 line 296
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6454 line 298
  70. def OAI.MUB6.Certificate.PairSemantics.raw6455 line 307
  71. def OAI.MUB6.Certificate.PairSemantics.raw6455step0 line 309
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6455 line 311
  73. def OAI.MUB6.Certificate.PairSemantics.raw6456 line 320
  74. def OAI.MUB6.Certificate.PairSemantics.raw6456step0 line 322
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6456 line 324
  76. def OAI.MUB6.Certificate.PairSemantics.raw6457 line 333
  77. def OAI.MUB6.Certificate.PairSemantics.raw6457step0 line 335
  78. def OAI.MUB6.Certificate.PairSemantics.raw6457step1 line 337
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6457 line 339
  80. def OAI.MUB6.Certificate.PairSemantics.raw6458 line 352
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6458 line 354
  82. def OAI.MUB6.Certificate.PairSemantics.raw6459 line 358
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6459 line 360
  84. def OAI.MUB6.Certificate.PairSemantics.raw6460 line 364
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6460 line 366
  86. def OAI.MUB6.Certificate.PairSemantics.raw6461 line 370
  87. def OAI.MUB6.Certificate.PairSemantics.raw6461step0 line 372
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical6461 line 374
  89. def OAI.MUB6.Certificate.PairSemantics.raw6462 line 383
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical6462 line 385
  91. def OAI.MUB6.Certificate.PairSemantics.raw6463 line 389
  92. def OAI.MUB6.Certificate.PairSemantics.raw6463step0 line 391
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical6463 line 393