OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical307.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9824 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw9824step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9824 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw9825 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw9825step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9825 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw9826 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw9826step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9826 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw9827 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw9827step0 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical9827 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw9828 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw9828step0 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical9828 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw9829 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw9829step0 line 82
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9829 line 84
  19. def OAI.MUB6.Certificate.PairSemantics.raw9830 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw9830step0 line 95
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9830 line 97
  22. def OAI.MUB6.Certificate.PairSemantics.raw9831 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw9831step0 line 108
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9831 line 110
  25. def OAI.MUB6.Certificate.PairSemantics.raw9832 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw9832step0 line 121
  27. def OAI.MUB6.Certificate.PairSemantics.raw9832step1 line 123
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical9832 line 125
  29. def OAI.MUB6.Certificate.PairSemantics.raw9833 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw9833step0 line 141
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical9833 line 143
  32. def OAI.MUB6.Certificate.PairSemantics.raw9834 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw9834step0 line 154
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical9834 line 156
  35. def OAI.MUB6.Certificate.PairSemantics.raw9835 line 165
  36. def OAI.MUB6.Certificate.PairSemantics.raw9835step0 line 167
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9835 line 169
  38. def OAI.MUB6.Certificate.PairSemantics.raw9836 line 178
  39. def OAI.MUB6.Certificate.PairSemantics.raw9836step0 line 180
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical9836 line 182
  41. def OAI.MUB6.Certificate.PairSemantics.raw9837 line 191
  42. def OAI.MUB6.Certificate.PairSemantics.raw9837step0 line 193
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical9837 line 195
  44. def OAI.MUB6.Certificate.PairSemantics.raw9838 line 204
  45. def OAI.MUB6.Certificate.PairSemantics.raw9838step0 line 206
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9838 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw9839 line 217
  48. def OAI.MUB6.Certificate.PairSemantics.raw9839step0 line 219
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical9839 line 221
  50. def OAI.MUB6.Certificate.PairSemantics.raw9840 line 230
  51. def OAI.MUB6.Certificate.PairSemantics.raw9840step0 line 232
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9840 line 234
  53. def OAI.MUB6.Certificate.PairSemantics.raw9841 line 243
  54. def OAI.MUB6.Certificate.PairSemantics.raw9841step0 line 245
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9841 line 247
  56. def OAI.MUB6.Certificate.PairSemantics.raw9842 line 256
  57. def OAI.MUB6.Certificate.PairSemantics.raw9842step0 line 258
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9842 line 260
  59. def OAI.MUB6.Certificate.PairSemantics.raw9843 line 269
  60. def OAI.MUB6.Certificate.PairSemantics.raw9843step0 line 271
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9843 line 273
  62. def OAI.MUB6.Certificate.PairSemantics.raw9844 line 282
  63. def OAI.MUB6.Certificate.PairSemantics.raw9844step0 line 284
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical9844 line 286
  65. def OAI.MUB6.Certificate.PairSemantics.raw9845 line 295
  66. def OAI.MUB6.Certificate.PairSemantics.raw9845step0 line 297
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9845 line 299
  68. def OAI.MUB6.Certificate.PairSemantics.raw9846 line 308
  69. def OAI.MUB6.Certificate.PairSemantics.raw9846step0 line 310
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical9846 line 312
  71. def OAI.MUB6.Certificate.PairSemantics.raw9847 line 321
  72. def OAI.MUB6.Certificate.PairSemantics.raw9847step0 line 323
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical9847 line 325
  74. def OAI.MUB6.Certificate.PairSemantics.raw9848 line 334
  75. def OAI.MUB6.Certificate.PairSemantics.raw9848step0 line 336
  76. def OAI.MUB6.Certificate.PairSemantics.raw9848step1 line 338
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9848 line 340
  78. def OAI.MUB6.Certificate.PairSemantics.raw9849 line 354
  79. def OAI.MUB6.Certificate.PairSemantics.raw9849step0 line 356
  80. def OAI.MUB6.Certificate.PairSemantics.raw9849step1 line 358
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical9849 line 360
  82. def OAI.MUB6.Certificate.PairSemantics.raw9850 line 373
  83. def OAI.MUB6.Certificate.PairSemantics.raw9850step0 line 375
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical9850 line 377
  85. def OAI.MUB6.Certificate.PairSemantics.raw9851 line 386
  86. def OAI.MUB6.Certificate.PairSemantics.raw9851step0 line 388
  87. def OAI.MUB6.Certificate.PairSemantics.raw9851step1 line 390
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9851 line 392
  89. def OAI.MUB6.Certificate.PairSemantics.raw9852 line 405
  90. def OAI.MUB6.Certificate.PairSemantics.raw9852step0 line 407
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical9852 line 409
  92. def OAI.MUB6.Certificate.PairSemantics.raw9853 line 418
  93. def OAI.MUB6.Certificate.PairSemantics.raw9853step0 line 420
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical9853 line 422
  95. def OAI.MUB6.Certificate.PairSemantics.raw9854 line 431
  96. def OAI.MUB6.Certificate.PairSemantics.raw9854step0 line 433
  97. def OAI.MUB6.Certificate.PairSemantics.raw9854step1 line 435
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9854 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw9855 line 450
  100. def OAI.MUB6.Certificate.PairSemantics.raw9855step0 line 452
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical9855 line 454