OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical46.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1472 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1472 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw1473 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1473 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw1474 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1474 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw1475 line 31
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1475 line 33
  9. def OAI.MUB6.Certificate.PairSemantics.raw1476 line 37
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1476 line 39
  11. def OAI.MUB6.Certificate.PairSemantics.raw1477 line 43
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1477 line 45
  13. def OAI.MUB6.Certificate.PairSemantics.raw1478 line 49
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1478 line 51
  15. def OAI.MUB6.Certificate.PairSemantics.raw1479 line 55
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1479 line 57
  17. def OAI.MUB6.Certificate.PairSemantics.raw1480 line 61
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1480 line 63
  19. def OAI.MUB6.Certificate.PairSemantics.raw1481 line 67
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1481 line 69
  21. def OAI.MUB6.Certificate.PairSemantics.raw1482 line 73
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1482 line 75
  23. def OAI.MUB6.Certificate.PairSemantics.raw1483 line 79
  24. def OAI.MUB6.Certificate.PairSemantics.raw1483step0 line 81
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1483 line 83
  26. def OAI.MUB6.Certificate.PairSemantics.raw1484 line 92
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1484 line 94
  28. def OAI.MUB6.Certificate.PairSemantics.raw1485 line 98
  29. def OAI.MUB6.Certificate.PairSemantics.raw1485step0 line 100
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1485 line 102
  31. def OAI.MUB6.Certificate.PairSemantics.raw1486 line 111
  32. def OAI.MUB6.Certificate.PairSemantics.raw1486step0 line 113
  33. def OAI.MUB6.Certificate.PairSemantics.raw1486step1 line 115
  34. def OAI.MUB6.Certificate.PairSemantics.raw1486step2 line 117
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1486 line 119
  36. def OAI.MUB6.Certificate.PairSemantics.raw1487 line 136
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1487 line 138
  38. def OAI.MUB6.Certificate.PairSemantics.raw1488 line 142
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1488 line 144
  40. def OAI.MUB6.Certificate.PairSemantics.raw1489 line 148
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1489 line 150
  42. def OAI.MUB6.Certificate.PairSemantics.raw1490 line 154
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1490 line 156
  44. def OAI.MUB6.Certificate.PairSemantics.raw1491 line 160
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1491 line 162
  46. def OAI.MUB6.Certificate.PairSemantics.raw1492 line 166
  47. def OAI.MUB6.Certificate.PairSemantics.raw1492step0 line 168
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1492 line 170
  49. def OAI.MUB6.Certificate.PairSemantics.raw1493 line 179
  50. def OAI.MUB6.Certificate.PairSemantics.raw1493step0 line 181
  51. def OAI.MUB6.Certificate.PairSemantics.raw1493step1 line 183
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1493 line 185
  53. def OAI.MUB6.Certificate.PairSemantics.raw1494 line 198
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical1494 line 200
  55. def OAI.MUB6.Certificate.PairSemantics.raw1495 line 204
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1495 line 206
  57. def OAI.MUB6.Certificate.PairSemantics.raw1496 line 210
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1496 line 212
  59. def OAI.MUB6.Certificate.PairSemantics.raw1497 line 216
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1497 line 218
  61. def OAI.MUB6.Certificate.PairSemantics.raw1498 line 222
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1498 line 224
  63. def OAI.MUB6.Certificate.PairSemantics.raw1499 line 228
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical1499 line 230
  65. def OAI.MUB6.Certificate.PairSemantics.raw1500 line 234
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1500 line 236
  67. def OAI.MUB6.Certificate.PairSemantics.raw1501 line 240
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1501 line 242
  69. def OAI.MUB6.Certificate.PairSemantics.raw1502 line 246
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1502 line 248
  71. def OAI.MUB6.Certificate.PairSemantics.raw1503 line 252
  72. def OAI.MUB6.Certificate.PairSemantics.raw1503step0 line 254
  73. def OAI.MUB6.Certificate.PairSemantics.raw1503step1 line 256
  74. def OAI.MUB6.Certificate.PairSemantics.raw1503step2 line 258
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1503 line 260