OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical124.lean

GitHub source file

100 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3968 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw3968step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw3968step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3968 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw3969 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw3969step0 line 40
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3969 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw3970 line 51
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3970 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw3971 line 57
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3971 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw3972 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw3972step0 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw3972step1 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3972 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw3973 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw3973step0 line 84
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3973 line 86
  19. def OAI.MUB6.Certificate.PairSemantics.raw3974 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw3974step0 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw3974step1 line 99
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3974 line 101
  23. def OAI.MUB6.Certificate.PairSemantics.raw3975 line 114
  24. def OAI.MUB6.Certificate.PairSemantics.raw3975step0 line 116
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical3975 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw3976 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw3976step0 line 129
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3976 line 131
  29. def OAI.MUB6.Certificate.PairSemantics.raw3977 line 140
  30. def OAI.MUB6.Certificate.PairSemantics.raw3977step0 line 142
  31. def OAI.MUB6.Certificate.PairSemantics.raw3977step1 line 144
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3977 line 146
  33. def OAI.MUB6.Certificate.PairSemantics.raw3978 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw3978step0 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw3978step1 line 163
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical3978 line 165
  37. def OAI.MUB6.Certificate.PairSemantics.raw3979 line 178
  38. def OAI.MUB6.Certificate.PairSemantics.raw3979step0 line 180
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3979 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw3980 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw3980step0 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw3980step1 line 195
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3980 line 197
  44. def OAI.MUB6.Certificate.PairSemantics.raw3981 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3981 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw3982 line 216
  47. def OAI.MUB6.Certificate.PairSemantics.raw3982step0 line 218
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical3982 line 220
  49. def OAI.MUB6.Certificate.PairSemantics.raw3983 line 229
  50. def OAI.MUB6.Certificate.PairSemantics.raw3983step0 line 231
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical3983 line 233
  52. def OAI.MUB6.Certificate.PairSemantics.raw3984 line 242
  53. def OAI.MUB6.Certificate.PairSemantics.raw3984step0 line 244
  54. def OAI.MUB6.Certificate.PairSemantics.raw3984step1 line 246
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3984 line 248
  56. def OAI.MUB6.Certificate.PairSemantics.raw3985 line 261
  57. def OAI.MUB6.Certificate.PairSemantics.raw3985step0 line 263
  58. def OAI.MUB6.Certificate.PairSemantics.raw3985step1 line 265
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3985 line 267
  60. def OAI.MUB6.Certificate.PairSemantics.raw3986 line 280
  61. def OAI.MUB6.Certificate.PairSemantics.raw3986step0 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw3986step1 line 284
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical3986 line 286
  64. def OAI.MUB6.Certificate.PairSemantics.raw3987 line 299
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3987 line 301
  66. def OAI.MUB6.Certificate.PairSemantics.raw3988 line 305
  67. def OAI.MUB6.Certificate.PairSemantics.raw3988step0 line 307
  68. def OAI.MUB6.Certificate.PairSemantics.raw3988step1 line 309
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3988 line 311
  70. def OAI.MUB6.Certificate.PairSemantics.raw3989 line 324
  71. def OAI.MUB6.Certificate.PairSemantics.raw3989step0 line 326
  72. def OAI.MUB6.Certificate.PairSemantics.raw3989step1 line 328
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3989 line 330
  74. def OAI.MUB6.Certificate.PairSemantics.raw3990 line 343
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3990 line 345
  76. def OAI.MUB6.Certificate.PairSemantics.raw3991 line 349
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3991 line 351
  78. def OAI.MUB6.Certificate.PairSemantics.raw3992 line 355
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical3992 line 357
  80. def OAI.MUB6.Certificate.PairSemantics.raw3993 line 361
  81. def OAI.MUB6.Certificate.PairSemantics.raw3993step0 line 363
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3993 line 365
  83. def OAI.MUB6.Certificate.PairSemantics.raw3994 line 374
  84. def OAI.MUB6.Certificate.PairSemantics.raw3994step0 line 376
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3994 line 378
  86. def OAI.MUB6.Certificate.PairSemantics.raw3995 line 387
  87. def OAI.MUB6.Certificate.PairSemantics.raw3995step0 line 389
  88. def OAI.MUB6.Certificate.PairSemantics.raw3995step1 line 391
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3995 line 393
  90. def OAI.MUB6.Certificate.PairSemantics.raw3996 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw3996step0 line 408
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3996 line 410
  93. def OAI.MUB6.Certificate.PairSemantics.raw3997 line 419
  94. def OAI.MUB6.Certificate.PairSemantics.raw3997step0 line 421
  95. def OAI.MUB6.Certificate.PairSemantics.raw3997step1 line 423
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3997 line 425
  97. def OAI.MUB6.Certificate.PairSemantics.raw3998 line 438
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3998 line 440
  99. def OAI.MUB6.Certificate.PairSemantics.raw3999 line 444
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3999 line 446