OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical50.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1600 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1600 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1601 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw1601step0 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1601 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw1602 line 35
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1602 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw1603 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw1603step0 line 43
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1603 line 45
  11. def OAI.MUB6.Certificate.PairSemantics.raw1604 line 54
  12. def OAI.MUB6.Certificate.PairSemantics.raw1604step0 line 56
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1604 line 58
  14. def OAI.MUB6.Certificate.PairSemantics.raw1605 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1605 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw1606 line 73
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1606 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw1607 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw1607step0 line 81
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1607 line 83
  21. def OAI.MUB6.Certificate.PairSemantics.raw1608 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw1608step0 line 94
  23. def OAI.MUB6.Certificate.PairSemantics.raw1608step1 line 96
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1608 line 98
  25. def OAI.MUB6.Certificate.PairSemantics.raw1609 line 111
  26. def OAI.MUB6.Certificate.PairSemantics.raw1609step0 line 113
  27. def OAI.MUB6.Certificate.PairSemantics.raw1609step1 line 115
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1609 line 117
  29. def OAI.MUB6.Certificate.PairSemantics.raw1610 line 130
  30. def OAI.MUB6.Certificate.PairSemantics.raw1610step0 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw1610step1 line 134
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1610 line 136
  33. def OAI.MUB6.Certificate.PairSemantics.raw1611 line 149
  34. def OAI.MUB6.Certificate.PairSemantics.raw1611step0 line 151
  35. def OAI.MUB6.Certificate.PairSemantics.raw1611step1 line 153
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1611 line 155
  37. def OAI.MUB6.Certificate.PairSemantics.raw1612 line 168
  38. def OAI.MUB6.Certificate.PairSemantics.raw1612step0 line 170
  39. def OAI.MUB6.Certificate.PairSemantics.raw1612step1 line 172
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1612 line 174
  41. def OAI.MUB6.Certificate.PairSemantics.raw1613 line 187
  42. def OAI.MUB6.Certificate.PairSemantics.raw1613step0 line 189
  43. def OAI.MUB6.Certificate.PairSemantics.raw1613step1 line 191
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1613 line 193
  45. def OAI.MUB6.Certificate.PairSemantics.raw1614 line 206
  46. def OAI.MUB6.Certificate.PairSemantics.raw1614step0 line 208
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1614 line 210
  48. def OAI.MUB6.Certificate.PairSemantics.raw1615 line 219
  49. def OAI.MUB6.Certificate.PairSemantics.raw1615step0 line 221
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1615 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw1616 line 232
  52. def OAI.MUB6.Certificate.PairSemantics.raw1616step0 line 234
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1616 line 236
  54. def OAI.MUB6.Certificate.PairSemantics.raw1617 line 245
  55. def OAI.MUB6.Certificate.PairSemantics.raw1617step0 line 247
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1617 line 249
  57. def OAI.MUB6.Certificate.PairSemantics.raw1618 line 258
  58. def OAI.MUB6.Certificate.PairSemantics.raw1618step0 line 260
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1618 line 262
  60. def OAI.MUB6.Certificate.PairSemantics.raw1619 line 271
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1619 line 273
  62. def OAI.MUB6.Certificate.PairSemantics.raw1620 line 277
  63. def OAI.MUB6.Certificate.PairSemantics.raw1620step0 line 279
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical1620 line 281
  65. def OAI.MUB6.Certificate.PairSemantics.raw1621 line 290
  66. def OAI.MUB6.Certificate.PairSemantics.raw1621step0 line 292
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1621 line 294
  68. def OAI.MUB6.Certificate.PairSemantics.raw1622 line 303
  69. def OAI.MUB6.Certificate.PairSemantics.raw1622step0 line 305
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1622 line 307
  71. def OAI.MUB6.Certificate.PairSemantics.raw1623 line 316
  72. def OAI.MUB6.Certificate.PairSemantics.raw1623step0 line 318
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1623 line 320
  74. def OAI.MUB6.Certificate.PairSemantics.raw1624 line 329
  75. def OAI.MUB6.Certificate.PairSemantics.raw1624step0 line 331
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1624 line 333
  77. def OAI.MUB6.Certificate.PairSemantics.raw1625 line 342
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1625 line 344
  79. def OAI.MUB6.Certificate.PairSemantics.raw1626 line 348
  80. def OAI.MUB6.Certificate.PairSemantics.raw1626step0 line 350
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical1626 line 352
  82. def OAI.MUB6.Certificate.PairSemantics.raw1627 line 361
  83. def OAI.MUB6.Certificate.PairSemantics.raw1627step0 line 363
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical1627 line 365
  85. def OAI.MUB6.Certificate.PairSemantics.raw1628 line 374
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1628 line 376
  87. def OAI.MUB6.Certificate.PairSemantics.raw1629 line 380
  88. def OAI.MUB6.Certificate.PairSemantics.raw1629step0 line 382
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1629 line 384
  90. def OAI.MUB6.Certificate.PairSemantics.raw1630 line 393
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical1630 line 395
  92. def OAI.MUB6.Certificate.PairSemantics.raw1631 line 399
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1631 line 401