OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical26.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw832 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw832step0 line 15
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical832 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw833 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw833step0 line 28
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical833 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw834 line 39
  8. def OAI.MUB6.Certificate.PairSemantics.raw834step0 line 41
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical834 line 43
  10. def OAI.MUB6.Certificate.PairSemantics.raw835 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw835step0 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw835step1 line 56
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical835 line 58
  14. def OAI.MUB6.Certificate.PairSemantics.raw836 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw836step0 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw836step1 line 75
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical836 line 77
  18. def OAI.MUB6.Certificate.PairSemantics.raw837 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw837step0 line 92
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical837 line 94
  21. def OAI.MUB6.Certificate.PairSemantics.raw838 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw838step0 line 105
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical838 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw839 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw839step0 line 118
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical839 line 120
  27. def OAI.MUB6.Certificate.PairSemantics.raw840 line 129
  28. def OAI.MUB6.Certificate.PairSemantics.raw840step0 line 131
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical840 line 133
  30. def OAI.MUB6.Certificate.PairSemantics.raw841 line 142
  31. def OAI.MUB6.Certificate.PairSemantics.raw841step0 line 144
  32. def OAI.MUB6.Certificate.PairSemantics.raw841step1 line 146
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical841 line 148
  34. def OAI.MUB6.Certificate.PairSemantics.raw842 line 161
  35. def OAI.MUB6.Certificate.PairSemantics.raw842step0 line 163
  36. def OAI.MUB6.Certificate.PairSemantics.raw842step1 line 165
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical842 line 167
  38. def OAI.MUB6.Certificate.PairSemantics.raw843 line 180
  39. def OAI.MUB6.Certificate.PairSemantics.raw843step0 line 182
  40. def OAI.MUB6.Certificate.PairSemantics.raw843step1 line 184
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical843 line 186
  42. def OAI.MUB6.Certificate.PairSemantics.raw844 line 199
  43. def OAI.MUB6.Certificate.PairSemantics.raw844step0 line 201
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical844 line 203
  45. def OAI.MUB6.Certificate.PairSemantics.raw845 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw845step0 line 215
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical845 line 217
  48. def OAI.MUB6.Certificate.PairSemantics.raw846 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw846step0 line 229
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical846 line 231
  51. def OAI.MUB6.Certificate.PairSemantics.raw847 line 241
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical847 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw848 line 247
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical848 line 249
  55. def OAI.MUB6.Certificate.PairSemantics.raw849 line 253
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical849 line 255
  57. def OAI.MUB6.Certificate.PairSemantics.raw850 line 259
  58. def OAI.MUB6.Certificate.PairSemantics.raw850step0 line 261
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical850 line 263
  60. def OAI.MUB6.Certificate.PairSemantics.raw851 line 272
  61. def OAI.MUB6.Certificate.PairSemantics.raw851step0 line 274
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical851 line 276
  63. def OAI.MUB6.Certificate.PairSemantics.raw852 line 285
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical852 line 287
  65. def OAI.MUB6.Certificate.PairSemantics.raw853 line 291
  66. def OAI.MUB6.Certificate.PairSemantics.raw853step0 line 293
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical853 line 295
  68. def OAI.MUB6.Certificate.PairSemantics.raw854 line 304
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical854 line 306
  70. def OAI.MUB6.Certificate.PairSemantics.raw855 line 310
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical855 line 312
  72. def OAI.MUB6.Certificate.PairSemantics.raw856 line 316
  73. def OAI.MUB6.Certificate.PairSemantics.raw856step0 line 318
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical856 line 320
  75. def OAI.MUB6.Certificate.PairSemantics.raw857 line 329
  76. def OAI.MUB6.Certificate.PairSemantics.raw857step0 line 331
  77. def OAI.MUB6.Certificate.PairSemantics.raw857step1 line 333
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical857 line 335
  79. def OAI.MUB6.Certificate.PairSemantics.raw858 line 350
  80. def OAI.MUB6.Certificate.PairSemantics.raw858step0 line 352
  81. def OAI.MUB6.Certificate.PairSemantics.raw858step1 line 354
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical858 line 356
  83. def OAI.MUB6.Certificate.PairSemantics.raw859 line 371
  84. def OAI.MUB6.Certificate.PairSemantics.raw859step0 line 373
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical859 line 375
  86. def OAI.MUB6.Certificate.PairSemantics.raw860 line 385
  87. def OAI.MUB6.Certificate.PairSemantics.raw860step0 line 387
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical860 line 389
  89. def OAI.MUB6.Certificate.PairSemantics.raw861 line 399
  90. def OAI.MUB6.Certificate.PairSemantics.raw861step0 line 401
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical861 line 403
  92. def OAI.MUB6.Certificate.PairSemantics.raw862 line 413
  93. def OAI.MUB6.Certificate.PairSemantics.raw862step0 line 415
  94. def OAI.MUB6.Certificate.PairSemantics.raw862step1 line 417
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical862 line 419
  96. def OAI.MUB6.Certificate.PairSemantics.raw863 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw863step0 line 435
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical863 line 437