OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical48.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1536 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw1536step0 line 13
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical1536 line 15
  4. def OAI.MUB6.Certificate.PairSemantics.raw1537 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1537step0 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1537 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw1538 line 37
  8. def OAI.MUB6.Certificate.PairSemantics.raw1538step0 line 39
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1538 line 41
  10. def OAI.MUB6.Certificate.PairSemantics.raw1539 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw1539step0 line 52
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1539 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw1540 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw1540step0 line 65
  15. def OAI.MUB6.Certificate.PairSemantics.raw1540step1 line 67
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1540 line 69
  17. def OAI.MUB6.Certificate.PairSemantics.raw1541 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw1541step0 line 85
  19. def OAI.MUB6.Certificate.PairSemantics.raw1541step1 line 87
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1541 line 89
  21. def OAI.MUB6.Certificate.PairSemantics.raw1542 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw1542step0 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw1542step1 line 107
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1542 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw1543 line 123
  26. def OAI.MUB6.Certificate.PairSemantics.raw1543step0 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw1543step1 line 127
  28. def OAI.MUB6.Certificate.PairSemantics.raw1543step2 line 129
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1543 line 131
  30. def OAI.MUB6.Certificate.PairSemantics.raw1544 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw1544step0 line 151
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1544 line 153
  33. def OAI.MUB6.Certificate.PairSemantics.raw1545 line 162
  34. def OAI.MUB6.Certificate.PairSemantics.raw1545step0 line 164
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1545 line 166
  36. def OAI.MUB6.Certificate.PairSemantics.raw1546 line 175
  37. def OAI.MUB6.Certificate.PairSemantics.raw1546step0 line 177
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1546 line 179
  39. def OAI.MUB6.Certificate.PairSemantics.raw1547 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw1547step0 line 190
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1547 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw1548 line 201
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1548 line 203
  44. def OAI.MUB6.Certificate.PairSemantics.raw1549 line 207
  45. def OAI.MUB6.Certificate.PairSemantics.raw1549step0 line 209
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1549 line 211
  47. def OAI.MUB6.Certificate.PairSemantics.raw1550 line 220
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1550 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw1551 line 226
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1551 line 228
  51. def OAI.MUB6.Certificate.PairSemantics.raw1552 line 232
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1552 line 234
  53. def OAI.MUB6.Certificate.PairSemantics.raw1553 line 238
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical1553 line 240
  55. def OAI.MUB6.Certificate.PairSemantics.raw1554 line 244
  56. def OAI.MUB6.Certificate.PairSemantics.raw1554step0 line 246
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1554 line 248
  58. def OAI.MUB6.Certificate.PairSemantics.raw1555 line 257
  59. def OAI.MUB6.Certificate.PairSemantics.raw1555step0 line 259
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1555 line 261
  61. def OAI.MUB6.Certificate.PairSemantics.raw1556 line 270
  62. def OAI.MUB6.Certificate.PairSemantics.raw1556step0 line 272
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1556 line 274
  64. def OAI.MUB6.Certificate.PairSemantics.raw1557 line 283
  65. def OAI.MUB6.Certificate.PairSemantics.raw1557step0 line 285
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1557 line 287
  67. def OAI.MUB6.Certificate.PairSemantics.raw1558 line 296
  68. def OAI.MUB6.Certificate.PairSemantics.raw1558step0 line 298
  69. def OAI.MUB6.Certificate.PairSemantics.raw1558step1 line 300
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1558 line 302
  71. def OAI.MUB6.Certificate.PairSemantics.raw1559 line 315
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1559 line 317
  73. def OAI.MUB6.Certificate.PairSemantics.raw1560 line 321
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1560 line 323
  75. def OAI.MUB6.Certificate.PairSemantics.raw1561 line 327
  76. def OAI.MUB6.Certificate.PairSemantics.raw1561step0 line 329
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1561 line 331
  78. def OAI.MUB6.Certificate.PairSemantics.raw1562 line 340
  79. def OAI.MUB6.Certificate.PairSemantics.raw1562step0 line 342
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1562 line 344
  81. def OAI.MUB6.Certificate.PairSemantics.raw1563 line 353
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1563 line 355
  83. def OAI.MUB6.Certificate.PairSemantics.raw1564 line 359
  84. def OAI.MUB6.Certificate.PairSemantics.raw1564step0 line 361
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1564 line 363
  86. def OAI.MUB6.Certificate.PairSemantics.raw1565 line 372
  87. def OAI.MUB6.Certificate.PairSemantics.raw1565step0 line 374
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical1565 line 376
  89. def OAI.MUB6.Certificate.PairSemantics.raw1566 line 385
  90. def OAI.MUB6.Certificate.PairSemantics.raw1566step0 line 387
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical1566 line 389
  92. def OAI.MUB6.Certificate.PairSemantics.raw1567 line 398
  93. def OAI.MUB6.Certificate.PairSemantics.raw1567step0 line 400
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical1567 line 402