OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical49.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1568 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw1568step0 line 16
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical1568 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw1569 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw1569step0 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1569 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw1570 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw1570step0 line 42
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1570 line 44
  10. def OAI.MUB6.Certificate.PairSemantics.raw1571 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw1571step0 line 55
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1571 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw1572 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw1572step0 line 68
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1572 line 70
  16. def OAI.MUB6.Certificate.PairSemantics.raw1573 line 79
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1573 line 81
  18. def OAI.MUB6.Certificate.PairSemantics.raw1574 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1574 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw1575 line 91
  21. def OAI.MUB6.Certificate.PairSemantics.raw1575step0 line 93
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1575 line 95
  23. def OAI.MUB6.Certificate.PairSemantics.raw1576 line 104
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1576 line 106
  25. def OAI.MUB6.Certificate.PairSemantics.raw1577 line 110
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1577 line 112
  27. def OAI.MUB6.Certificate.PairSemantics.raw1578 line 116
  28. def OAI.MUB6.Certificate.PairSemantics.raw1578step0 line 118
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1578 line 120
  30. def OAI.MUB6.Certificate.PairSemantics.raw1579 line 129
  31. def OAI.MUB6.Certificate.PairSemantics.raw1579step0 line 131
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1579 line 133
  33. def OAI.MUB6.Certificate.PairSemantics.raw1580 line 142
  34. def OAI.MUB6.Certificate.PairSemantics.raw1580step0 line 144
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1580 line 146
  36. def OAI.MUB6.Certificate.PairSemantics.raw1581 line 155
  37. def OAI.MUB6.Certificate.PairSemantics.raw1581step0 line 157
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1581 line 159
  39. def OAI.MUB6.Certificate.PairSemantics.raw1582 line 168
  40. def OAI.MUB6.Certificate.PairSemantics.raw1582step0 line 170
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1582 line 172
  42. def OAI.MUB6.Certificate.PairSemantics.raw1583 line 181
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1583 line 183
  44. def OAI.MUB6.Certificate.PairSemantics.raw1584 line 187
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1584 line 189
  46. def OAI.MUB6.Certificate.PairSemantics.raw1585 line 193
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1585 line 195
  48. def OAI.MUB6.Certificate.PairSemantics.raw1586 line 199
  49. def OAI.MUB6.Certificate.PairSemantics.raw1586step0 line 201
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1586 line 203
  51. def OAI.MUB6.Certificate.PairSemantics.raw1587 line 212
  52. def OAI.MUB6.Certificate.PairSemantics.raw1587step0 line 214
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1587 line 216
  54. def OAI.MUB6.Certificate.PairSemantics.raw1588 line 225
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1588 line 227
  56. def OAI.MUB6.Certificate.PairSemantics.raw1589 line 231
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1589 line 233
  58. def OAI.MUB6.Certificate.PairSemantics.raw1590 line 237
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1590 line 239
  60. def OAI.MUB6.Certificate.PairSemantics.raw1591 line 243
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1591 line 245
  62. def OAI.MUB6.Certificate.PairSemantics.raw1592 line 249
  63. def OAI.MUB6.Certificate.PairSemantics.raw1592step0 line 251
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical1592 line 253
  65. def OAI.MUB6.Certificate.PairSemantics.raw1593 line 262
  66. def OAI.MUB6.Certificate.PairSemantics.raw1593step0 line 264
  67. def OAI.MUB6.Certificate.PairSemantics.raw1593step1 line 266
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1593 line 268
  69. def OAI.MUB6.Certificate.PairSemantics.raw1594 line 281
  70. def OAI.MUB6.Certificate.PairSemantics.raw1594step0 line 283
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1594 line 285
  72. def OAI.MUB6.Certificate.PairSemantics.raw1595 line 294
  73. def OAI.MUB6.Certificate.PairSemantics.raw1595step0 line 296
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1595 line 298
  75. def OAI.MUB6.Certificate.PairSemantics.raw1596 line 307
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1596 line 309
  77. def OAI.MUB6.Certificate.PairSemantics.raw1597 line 313
  78. def OAI.MUB6.Certificate.PairSemantics.raw1597step0 line 315
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical1597 line 317
  80. def OAI.MUB6.Certificate.PairSemantics.raw1598 line 326
  81. def OAI.MUB6.Certificate.PairSemantics.raw1598step0 line 328
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1598 line 330
  83. def OAI.MUB6.Certificate.PairSemantics.raw1599 line 339
  84. def OAI.MUB6.Certificate.PairSemantics.raw1599step0 line 341
  85. def OAI.MUB6.Certificate.PairSemantics.raw1599step1 line 343
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1599 line 345