OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical224.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7168 line 20
  2. def OAI.MUB6.Certificate.PairSemantics.raw7168step0 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw7168step1 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7168 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw7169 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw7169step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw7169step1 line 43
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7169 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw7170 line 58
  10. def OAI.MUB6.Certificate.PairSemantics.raw7170step0 line 60
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical7170 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw7171 line 71
  13. def OAI.MUB6.Certificate.PairSemantics.raw7171step0 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw7171step1 line 75
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical7171 line 77
  16. def OAI.MUB6.Certificate.PairSemantics.raw7172 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw7172step0 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw7172step1 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw7172step2 line 96
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7172 line 98
  21. def OAI.MUB6.Certificate.PairSemantics.raw7173 line 115
  22. def OAI.MUB6.Certificate.PairSemantics.raw7173step0 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw7173step1 line 119
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical7173 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw7174 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw7174step0 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw7174step1 line 138
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7174 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw7175 line 153
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7175 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw7176 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw7176step0 line 161
  33. def OAI.MUB6.Certificate.PairSemantics.raw7176step1 line 163
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7176 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw7177 line 178
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7177 line 180
  37. def OAI.MUB6.Certificate.PairSemantics.raw7178 line 184
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7178 line 186
  39. def OAI.MUB6.Certificate.PairSemantics.raw7179 line 190
  40. def OAI.MUB6.Certificate.PairSemantics.raw7179step0 line 192
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical7179 line 194
  42. def OAI.MUB6.Certificate.PairSemantics.raw7180 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw7180step0 line 205
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7180 line 207
  45. def OAI.MUB6.Certificate.PairSemantics.raw7181 line 216
  46. def OAI.MUB6.Certificate.PairSemantics.raw7181step0 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw7181step1 line 220
  48. def OAI.MUB6.Certificate.PairSemantics.raw7181step2 line 222
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical7181 line 224
  50. def OAI.MUB6.Certificate.PairSemantics.raw7182 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw7182step0 line 243
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7182 line 245
  53. def OAI.MUB6.Certificate.PairSemantics.raw7183 line 254
  54. def OAI.MUB6.Certificate.PairSemantics.raw7183step0 line 256
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7183 line 258
  56. def OAI.MUB6.Certificate.PairSemantics.raw7184 line 267
  57. def OAI.MUB6.Certificate.PairSemantics.raw7184step0 line 269
  58. def OAI.MUB6.Certificate.PairSemantics.raw7184step1 line 271
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7184 line 273
  60. def OAI.MUB6.Certificate.PairSemantics.raw7185 line 286
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7185 line 288
  62. def OAI.MUB6.Certificate.PairSemantics.raw7186 line 292
  63. def OAI.MUB6.Certificate.PairSemantics.raw7186step0 line 294
  64. def OAI.MUB6.Certificate.PairSemantics.raw7186step1 line 296
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7186 line 298
  66. def OAI.MUB6.Certificate.PairSemantics.raw7187 line 311
  67. def OAI.MUB6.Certificate.PairSemantics.raw7187step0 line 313
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical7187 line 315
  69. def OAI.MUB6.Certificate.PairSemantics.raw7188 line 325
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7188 line 327
  71. def OAI.MUB6.Certificate.PairSemantics.raw7189 line 331
  72. def OAI.MUB6.Certificate.PairSemantics.raw7189step0 line 333
  73. def OAI.MUB6.Certificate.PairSemantics.raw7189step1 line 335
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7189 line 337
  75. def OAI.MUB6.Certificate.PairSemantics.raw7190 line 350
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7190 line 352
  77. def OAI.MUB6.Certificate.PairSemantics.raw7191 line 356
  78. def OAI.MUB6.Certificate.PairSemantics.raw7191step0 line 358
  79. def OAI.MUB6.Certificate.PairSemantics.raw7191step1 line 360
  80. def OAI.MUB6.Certificate.PairSemantics.raw7191step2 line 362
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical7191 line 364
  82. def OAI.MUB6.Certificate.PairSemantics.raw7192 line 382
  83. def OAI.MUB6.Certificate.PairSemantics.raw7192step0 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw7192step1 line 386
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7192 line 388
  86. def OAI.MUB6.Certificate.PairSemantics.raw7193 line 401
  87. def OAI.MUB6.Certificate.PairSemantics.raw7193step0 line 403
  88. def OAI.MUB6.Certificate.PairSemantics.raw7193step1 line 405
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7193 line 407
  90. def OAI.MUB6.Certificate.PairSemantics.raw7194 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw7194step0 line 422
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7194 line 424
  93. def OAI.MUB6.Certificate.PairSemantics.raw7195 line 433
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7195 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw7196 line 439
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7196 line 441
  97. def OAI.MUB6.Certificate.PairSemantics.raw7197 line 445
  98. def OAI.MUB6.Certificate.PairSemantics.raw7197step0 line 447
  99. def OAI.MUB6.Certificate.PairSemantics.raw7197step1 line 449
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical7197 line 451
  101. def OAI.MUB6.Certificate.PairSemantics.raw7198 line 464
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical7198 line 466
  103. def OAI.MUB6.Certificate.PairSemantics.raw7199 line 470
  104. def OAI.MUB6.Certificate.PairSemantics.raw7199step0 line 472
  105. def OAI.MUB6.Certificate.PairSemantics.raw7199step1 line 474
  106. def OAI.MUB6.Certificate.PairSemantics.raw7199step2 line 476
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7199 line 478