OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical218.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6976 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw6976step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw6976step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical6976 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw6977 line 37
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6977 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw6978 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw6978step0 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw6978step1 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw6978step2 line 49
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6978 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw6979 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw6979step0 line 70
  14. def OAI.MUB6.Certificate.PairSemantics.raw6979step1 line 72
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6979 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw6980 line 87
  17. def OAI.MUB6.Certificate.PairSemantics.raw6980step0 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw6980step1 line 91
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6980 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw6981 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw6981step0 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw6981step1 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical6981 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw6982 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6982 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw6983 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw6983step0 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw6983step1 line 135
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6983 line 137
  30. def OAI.MUB6.Certificate.PairSemantics.raw6984 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw6984step0 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw6984step1 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw6984step2 line 156
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical6984 line 158
  35. def OAI.MUB6.Certificate.PairSemantics.raw6985 line 175
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6985 line 177
  37. def OAI.MUB6.Certificate.PairSemantics.raw6986 line 181
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical6986 line 183
  39. def OAI.MUB6.Certificate.PairSemantics.raw6987 line 187
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical6987 line 189
  41. def OAI.MUB6.Certificate.PairSemantics.raw6988 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw6988step0 line 195
  43. def OAI.MUB6.Certificate.PairSemantics.raw6988step1 line 197
  44. def OAI.MUB6.Certificate.PairSemantics.raw6988step2 line 199
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical6988 line 201
  46. def OAI.MUB6.Certificate.PairSemantics.raw6989 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw6989step0 line 220
  48. def OAI.MUB6.Certificate.PairSemantics.raw6989step1 line 222
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical6989 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw6990 line 237
  51. def OAI.MUB6.Certificate.PairSemantics.raw6990step0 line 239
  52. def OAI.MUB6.Certificate.PairSemantics.raw6990step1 line 241
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical6990 line 243
  54. def OAI.MUB6.Certificate.PairSemantics.raw6991 line 256
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6991 line 258
  56. def OAI.MUB6.Certificate.PairSemantics.raw6992 line 262
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6992 line 264
  58. def OAI.MUB6.Certificate.PairSemantics.raw6993 line 268
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6993 line 270
  60. def OAI.MUB6.Certificate.PairSemantics.raw6994 line 274
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical6994 line 276
  62. def OAI.MUB6.Certificate.PairSemantics.raw6995 line 280
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6995 line 282
  64. def OAI.MUB6.Certificate.PairSemantics.raw6996 line 286
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6996 line 288
  66. def OAI.MUB6.Certificate.PairSemantics.raw6997 line 292
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical6997 line 294
  68. def OAI.MUB6.Certificate.PairSemantics.raw6998 line 298
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6998 line 300
  70. def OAI.MUB6.Certificate.PairSemantics.raw6999 line 304
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical6999 line 306
  72. def OAI.MUB6.Certificate.PairSemantics.raw7000 line 310
  73. def OAI.MUB6.Certificate.PairSemantics.raw7000step0 line 312
  74. def OAI.MUB6.Certificate.PairSemantics.raw7000step1 line 314
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7000 line 316
  76. def OAI.MUB6.Certificate.PairSemantics.raw7001 line 329
  77. def OAI.MUB6.Certificate.PairSemantics.raw7001step0 line 331
  78. def OAI.MUB6.Certificate.PairSemantics.raw7001step1 line 333
  79. def OAI.MUB6.Certificate.PairSemantics.raw7001step2 line 335
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7001 line 337
  81. def OAI.MUB6.Certificate.PairSemantics.raw7002 line 354
  82. def OAI.MUB6.Certificate.PairSemantics.raw7002step0 line 356
  83. def OAI.MUB6.Certificate.PairSemantics.raw7002step1 line 358
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7002 line 360
  85. def OAI.MUB6.Certificate.PairSemantics.raw7003 line 373
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical7003 line 375
  87. def OAI.MUB6.Certificate.PairSemantics.raw7004 line 379
  88. def OAI.MUB6.Certificate.PairSemantics.raw7004step0 line 381
  89. def OAI.MUB6.Certificate.PairSemantics.raw7004step1 line 383
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical7004 line 385
  91. def OAI.MUB6.Certificate.PairSemantics.raw7005 line 398
  92. def OAI.MUB6.Certificate.PairSemantics.raw7005step0 line 400
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7005 line 402
  94. def OAI.MUB6.Certificate.PairSemantics.raw7006 line 411
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7006 line 413
  96. def OAI.MUB6.Certificate.PairSemantics.raw7007 line 417
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7007 line 419