OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical22.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw704 line 19
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical704 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw705 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical705 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw706 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical706 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw707 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical707 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw708 line 43
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical708 line 45
  11. def OAI.MUB6.Certificate.PairSemantics.raw709 line 49
  12. def OAI.MUB6.Certificate.PairSemantics.raw709step0 line 51
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical709 line 53
  14. def OAI.MUB6.Certificate.PairSemantics.raw710 line 62
  15. def OAI.MUB6.Certificate.PairSemantics.raw710step0 line 64
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical710 line 66
  17. def OAI.MUB6.Certificate.PairSemantics.raw711 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw711step0 line 77
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical711 line 79
  20. def OAI.MUB6.Certificate.PairSemantics.raw712 line 88
  21. def OAI.MUB6.Certificate.PairSemantics.raw712step0 line 90
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical712 line 92
  23. def OAI.MUB6.Certificate.PairSemantics.raw713 line 101
  24. def OAI.MUB6.Certificate.PairSemantics.raw713step0 line 103
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical713 line 105
  26. def OAI.MUB6.Certificate.PairSemantics.raw714 line 114
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical714 line 116
  28. def OAI.MUB6.Certificate.PairSemantics.raw715 line 120
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical715 line 122
  30. def OAI.MUB6.Certificate.PairSemantics.raw716 line 126
  31. def OAI.MUB6.Certificate.PairSemantics.raw716step0 line 128
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical716 line 130
  33. def OAI.MUB6.Certificate.PairSemantics.raw717 line 139
  34. def OAI.MUB6.Certificate.PairSemantics.raw717step0 line 141
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical717 line 143
  36. def OAI.MUB6.Certificate.PairSemantics.raw718 line 152
  37. def OAI.MUB6.Certificate.PairSemantics.raw718step0 line 154
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical718 line 156
  39. def OAI.MUB6.Certificate.PairSemantics.raw719 line 165
  40. def OAI.MUB6.Certificate.PairSemantics.raw719step0 line 167
  41. def OAI.MUB6.Certificate.PairSemantics.raw719step1 line 169
  42. def OAI.MUB6.Certificate.PairSemantics.raw719step2 line 171
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical719 line 173
  44. def OAI.MUB6.Certificate.PairSemantics.raw720 line 190
  45. def OAI.MUB6.Certificate.PairSemantics.raw720step0 line 192
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical720 line 194
  47. def OAI.MUB6.Certificate.PairSemantics.raw721 line 203
  48. def OAI.MUB6.Certificate.PairSemantics.raw721step0 line 205
  49. def OAI.MUB6.Certificate.PairSemantics.raw721step1 line 207
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical721 line 209
  51. def OAI.MUB6.Certificate.PairSemantics.raw722 line 222
  52. def OAI.MUB6.Certificate.PairSemantics.raw722step0 line 224
  53. def OAI.MUB6.Certificate.PairSemantics.raw722step1 line 226
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical722 line 228
  55. def OAI.MUB6.Certificate.PairSemantics.raw723 line 241
  56. def OAI.MUB6.Certificate.PairSemantics.raw723step0 line 243
  57. def OAI.MUB6.Certificate.PairSemantics.raw723step1 line 245
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical723 line 247
  59. def OAI.MUB6.Certificate.PairSemantics.raw724 line 261
  60. def OAI.MUB6.Certificate.PairSemantics.raw724step0 line 263
  61. def OAI.MUB6.Certificate.PairSemantics.raw724step1 line 265
  62. def OAI.MUB6.Certificate.PairSemantics.raw724step2 line 267
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical724 line 269
  64. def OAI.MUB6.Certificate.PairSemantics.raw725 line 287
  65. def OAI.MUB6.Certificate.PairSemantics.raw725step0 line 289
  66. def OAI.MUB6.Certificate.PairSemantics.raw725step1 line 291
  67. def OAI.MUB6.Certificate.PairSemantics.raw725step2 line 293
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical725 line 295
  69. def OAI.MUB6.Certificate.PairSemantics.raw726 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw726step0 line 315
  71. def OAI.MUB6.Certificate.PairSemantics.raw726step1 line 317
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical726 line 319
  73. def OAI.MUB6.Certificate.PairSemantics.raw727 line 333
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical727 line 335
  75. def OAI.MUB6.Certificate.PairSemantics.raw728 line 339
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical728 line 341
  77. def OAI.MUB6.Certificate.PairSemantics.raw729 line 345
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical729 line 347
  79. def OAI.MUB6.Certificate.PairSemantics.raw730 line 351
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical730 line 353
  81. def OAI.MUB6.Certificate.PairSemantics.raw731 line 357
  82. def OAI.MUB6.Certificate.PairSemantics.raw731step0 line 359
  83. def OAI.MUB6.Certificate.PairSemantics.raw731step1 line 361
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical731 line 363
  85. def OAI.MUB6.Certificate.PairSemantics.raw732 line 376
  86. def OAI.MUB6.Certificate.PairSemantics.raw732step0 line 378
  87. def OAI.MUB6.Certificate.PairSemantics.raw732step1 line 380
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical732 line 382
  89. def OAI.MUB6.Certificate.PairSemantics.raw733 line 395
  90. def OAI.MUB6.Certificate.PairSemantics.raw733step0 line 397
  91. def OAI.MUB6.Certificate.PairSemantics.raw733step1 line 399
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical733 line 401
  93. def OAI.MUB6.Certificate.PairSemantics.raw734 line 414
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical734 line 416
  95. def OAI.MUB6.Certificate.PairSemantics.raw735 line 420
  96. def OAI.MUB6.Certificate.PairSemantics.raw735step0 line 422
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical735 line 424