OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical126.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4032 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4032 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw4033 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw4033step0 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical4033 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw4034 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4034 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw4035 line 41
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4035 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw4036 line 47
  11. def OAI.MUB6.Certificate.PairSemantics.raw4036step0 line 49
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical4036 line 51
  13. def OAI.MUB6.Certificate.PairSemantics.raw4037 line 60
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical4037 line 62
  15. def OAI.MUB6.Certificate.PairSemantics.raw4038 line 66
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical4038 line 68
  17. def OAI.MUB6.Certificate.PairSemantics.raw4039 line 72
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical4039 line 74
  19. def OAI.MUB6.Certificate.PairSemantics.raw4040 line 78
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical4040 line 80
  21. def OAI.MUB6.Certificate.PairSemantics.raw4041 line 84
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical4041 line 86
  23. def OAI.MUB6.Certificate.PairSemantics.raw4042 line 90
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical4042 line 92
  25. def OAI.MUB6.Certificate.PairSemantics.raw4043 line 96
  26. def OAI.MUB6.Certificate.PairSemantics.raw4043step0 line 98
  27. def OAI.MUB6.Certificate.PairSemantics.raw4043step1 line 100
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4043 line 102
  29. def OAI.MUB6.Certificate.PairSemantics.raw4044 line 115
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical4044 line 117
  31. def OAI.MUB6.Certificate.PairSemantics.raw4045 line 121
  32. def OAI.MUB6.Certificate.PairSemantics.raw4045step0 line 123
  33. def OAI.MUB6.Certificate.PairSemantics.raw4045step1 line 125
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4045 line 127
  35. def OAI.MUB6.Certificate.PairSemantics.raw4046 line 140
  36. def OAI.MUB6.Certificate.PairSemantics.raw4046step0 line 142
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical4046 line 144
  38. def OAI.MUB6.Certificate.PairSemantics.raw4047 line 153
  39. def OAI.MUB6.Certificate.PairSemantics.raw4047step0 line 155
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4047 line 157
  41. def OAI.MUB6.Certificate.PairSemantics.raw4048 line 166
  42. def OAI.MUB6.Certificate.PairSemantics.raw4048step0 line 168
  43. def OAI.MUB6.Certificate.PairSemantics.raw4048step1 line 170
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4048 line 172
  45. def OAI.MUB6.Certificate.PairSemantics.raw4049 line 185
  46. def OAI.MUB6.Certificate.PairSemantics.raw4049step0 line 187
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4049 line 189
  48. def OAI.MUB6.Certificate.PairSemantics.raw4050 line 198
  49. def OAI.MUB6.Certificate.PairSemantics.raw4050step0 line 200
  50. def OAI.MUB6.Certificate.PairSemantics.raw4050step1 line 202
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4050 line 204
  52. def OAI.MUB6.Certificate.PairSemantics.raw4051 line 217
  53. def OAI.MUB6.Certificate.PairSemantics.raw4051step0 line 219
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical4051 line 221
  55. def OAI.MUB6.Certificate.PairSemantics.raw4052 line 230
  56. def OAI.MUB6.Certificate.PairSemantics.raw4052step0 line 232
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical4052 line 234
  58. def OAI.MUB6.Certificate.PairSemantics.raw4053 line 243
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical4053 line 245
  60. def OAI.MUB6.Certificate.PairSemantics.raw4054 line 249
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4054 line 251
  62. def OAI.MUB6.Certificate.PairSemantics.raw4055 line 255
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical4055 line 257
  64. def OAI.MUB6.Certificate.PairSemantics.raw4056 line 261
  65. def OAI.MUB6.Certificate.PairSemantics.raw4056step0 line 263
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical4056 line 265
  67. def OAI.MUB6.Certificate.PairSemantics.raw4057 line 274
  68. def OAI.MUB6.Certificate.PairSemantics.raw4057step0 line 276
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4057 line 278
  70. def OAI.MUB6.Certificate.PairSemantics.raw4058 line 287
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical4058 line 289
  72. def OAI.MUB6.Certificate.PairSemantics.raw4059 line 293
  73. def OAI.MUB6.Certificate.PairSemantics.raw4059step0 line 295
  74. def OAI.MUB6.Certificate.PairSemantics.raw4059step1 line 297
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4059 line 299
  76. def OAI.MUB6.Certificate.PairSemantics.raw4060 line 312
  77. def OAI.MUB6.Certificate.PairSemantics.raw4060step0 line 314
  78. def OAI.MUB6.Certificate.PairSemantics.raw4060step1 line 316
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4060 line 318
  80. def OAI.MUB6.Certificate.PairSemantics.raw4061 line 332
  81. def OAI.MUB6.Certificate.PairSemantics.raw4061step0 line 334
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4061 line 336
  83. def OAI.MUB6.Certificate.PairSemantics.raw4062 line 346
  84. def OAI.MUB6.Certificate.PairSemantics.raw4062step0 line 348
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4062 line 350
  86. def OAI.MUB6.Certificate.PairSemantics.raw4063 line 360
  87. def OAI.MUB6.Certificate.PairSemantics.raw4063step0 line 362
  88. def OAI.MUB6.Certificate.PairSemantics.raw4063step1 line 364
  89. def OAI.MUB6.Certificate.PairSemantics.raw4063step2 line 366
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical4063 line 368