OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical24.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw768 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw768step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw768step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical768 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw769 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw769step0 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw769step1 line 38
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical769 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw770 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw770step0 line 55
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical770 line 57
  12. def OAI.MUB6.Certificate.PairSemantics.raw771 line 66
  13. def OAI.MUB6.Certificate.PairSemantics.raw771step0 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw771step1 line 70
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical771 line 72
  16. def OAI.MUB6.Certificate.PairSemantics.raw772 line 85
  17. def OAI.MUB6.Certificate.PairSemantics.raw772step0 line 87
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical772 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw773 line 98
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical773 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw774 line 104
  22. def OAI.MUB6.Certificate.PairSemantics.raw774step0 line 106
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical774 line 108
  24. def OAI.MUB6.Certificate.PairSemantics.raw775 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical775 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw776 line 123
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical776 line 125
  28. def OAI.MUB6.Certificate.PairSemantics.raw777 line 129
  29. def OAI.MUB6.Certificate.PairSemantics.raw777step0 line 131
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical777 line 133
  31. def OAI.MUB6.Certificate.PairSemantics.raw778 line 142
  32. def OAI.MUB6.Certificate.PairSemantics.raw778step0 line 144
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical778 line 146
  34. def OAI.MUB6.Certificate.PairSemantics.raw779 line 155
  35. def OAI.MUB6.Certificate.PairSemantics.raw779step0 line 157
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical779 line 159
  37. def OAI.MUB6.Certificate.PairSemantics.raw780 line 168
  38. def OAI.MUB6.Certificate.PairSemantics.raw780step0 line 170
  39. def OAI.MUB6.Certificate.PairSemantics.raw780step1 line 172
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical780 line 174
  41. def OAI.MUB6.Certificate.PairSemantics.raw781 line 187
  42. def OAI.MUB6.Certificate.PairSemantics.raw781step0 line 189
  43. def OAI.MUB6.Certificate.PairSemantics.raw781step1 line 191
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical781 line 193
  45. def OAI.MUB6.Certificate.PairSemantics.raw782 line 206
  46. def OAI.MUB6.Certificate.PairSemantics.raw782step0 line 208
  47. def OAI.MUB6.Certificate.PairSemantics.raw782step1 line 210
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical782 line 212
  49. def OAI.MUB6.Certificate.PairSemantics.raw783 line 225
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical783 line 227
  51. def OAI.MUB6.Certificate.PairSemantics.raw784 line 231
  52. def OAI.MUB6.Certificate.PairSemantics.raw784step0 line 233
  53. def OAI.MUB6.Certificate.PairSemantics.raw784step1 line 235
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical784 line 237
  55. def OAI.MUB6.Certificate.PairSemantics.raw785 line 250
  56. def OAI.MUB6.Certificate.PairSemantics.raw785step0 line 252
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical785 line 254
  58. def OAI.MUB6.Certificate.PairSemantics.raw786 line 263
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical786 line 265
  60. def OAI.MUB6.Certificate.PairSemantics.raw787 line 269
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical787 line 271
  62. def OAI.MUB6.Certificate.PairSemantics.raw788 line 275
  63. def OAI.MUB6.Certificate.PairSemantics.raw788step0 line 277
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical788 line 279
  65. def OAI.MUB6.Certificate.PairSemantics.raw789 line 288
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical789 line 290
  67. def OAI.MUB6.Certificate.PairSemantics.raw790 line 294
  68. def OAI.MUB6.Certificate.PairSemantics.raw790step0 line 296
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical790 line 298
  70. def OAI.MUB6.Certificate.PairSemantics.raw791 line 307
  71. def OAI.MUB6.Certificate.PairSemantics.raw791step0 line 309
  72. def OAI.MUB6.Certificate.PairSemantics.raw791step1 line 311
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical791 line 313
  74. def OAI.MUB6.Certificate.PairSemantics.raw792 line 326
  75. def OAI.MUB6.Certificate.PairSemantics.raw792step0 line 328
  76. def OAI.MUB6.Certificate.PairSemantics.raw792step1 line 330
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical792 line 332
  78. def OAI.MUB6.Certificate.PairSemantics.raw793 line 345
  79. def OAI.MUB6.Certificate.PairSemantics.raw793step0 line 347
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical793 line 349
  81. def OAI.MUB6.Certificate.PairSemantics.raw794 line 358
  82. def OAI.MUB6.Certificate.PairSemantics.raw794step0 line 360
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical794 line 362
  84. def OAI.MUB6.Certificate.PairSemantics.raw795 line 371
  85. def OAI.MUB6.Certificate.PairSemantics.raw795step0 line 373
  86. def OAI.MUB6.Certificate.PairSemantics.raw795step1 line 375
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical795 line 377
  88. def OAI.MUB6.Certificate.PairSemantics.raw796 line 390
  89. def OAI.MUB6.Certificate.PairSemantics.raw796step0 line 392
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical796 line 394
  91. def OAI.MUB6.Certificate.PairSemantics.raw797 line 403
  92. def OAI.MUB6.Certificate.PairSemantics.raw797step0 line 405
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical797 line 407
  94. def OAI.MUB6.Certificate.PairSemantics.raw798 line 416
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical798 line 418
  96. def OAI.MUB6.Certificate.PairSemantics.raw799 line 422
  97. def OAI.MUB6.Certificate.PairSemantics.raw799step0 line 424
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical799 line 426