OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical44.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1408 line 10
  2. def OAI.MUB6.Certificate.PairSemantics.raw1408step0 line 12
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical1408 line 14
  4. def OAI.MUB6.Certificate.PairSemantics.raw1409 line 23
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1409 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw1410 line 29
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1410 line 31
  8. def OAI.MUB6.Certificate.PairSemantics.raw1411 line 35
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1411 line 37
  10. def OAI.MUB6.Certificate.PairSemantics.raw1412 line 41
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1412 line 43
  12. def OAI.MUB6.Certificate.PairSemantics.raw1413 line 47
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1413 line 49
  14. def OAI.MUB6.Certificate.PairSemantics.raw1414 line 53
  15. def OAI.MUB6.Certificate.PairSemantics.raw1414step0 line 55
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1414 line 57
  17. def OAI.MUB6.Certificate.PairSemantics.raw1415 line 66
  18. def OAI.MUB6.Certificate.PairSemantics.raw1415step0 line 68
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1415 line 70
  20. def OAI.MUB6.Certificate.PairSemantics.raw1416 line 79
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1416 line 81
  22. def OAI.MUB6.Certificate.PairSemantics.raw1417 line 85
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1417 line 87
  24. def OAI.MUB6.Certificate.PairSemantics.raw1418 line 91
  25. def OAI.MUB6.Certificate.PairSemantics.raw1418step0 line 93
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1418 line 95
  27. def OAI.MUB6.Certificate.PairSemantics.raw1419 line 104
  28. def OAI.MUB6.Certificate.PairSemantics.raw1419step0 line 106
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1419 line 108
  30. def OAI.MUB6.Certificate.PairSemantics.raw1420 line 117
  31. def OAI.MUB6.Certificate.PairSemantics.raw1420step0 line 119
  32. def OAI.MUB6.Certificate.PairSemantics.raw1420step1 line 121
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1420 line 123
  34. def OAI.MUB6.Certificate.PairSemantics.raw1421 line 136
  35. def OAI.MUB6.Certificate.PairSemantics.raw1421step0 line 138
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1421 line 140
  37. def OAI.MUB6.Certificate.PairSemantics.raw1422 line 149
  38. def OAI.MUB6.Certificate.PairSemantics.raw1422step0 line 151
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1422 line 153
  40. def OAI.MUB6.Certificate.PairSemantics.raw1423 line 162
  41. def OAI.MUB6.Certificate.PairSemantics.raw1423step0 line 164
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1423 line 166
  43. def OAI.MUB6.Certificate.PairSemantics.raw1424 line 176
  44. def OAI.MUB6.Certificate.PairSemantics.raw1424step0 line 178
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1424 line 180
  46. def OAI.MUB6.Certificate.PairSemantics.raw1425 line 189
  47. def OAI.MUB6.Certificate.PairSemantics.raw1425step0 line 191
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1425 line 193
  49. def OAI.MUB6.Certificate.PairSemantics.raw1426 line 202
  50. def OAI.MUB6.Certificate.PairSemantics.raw1426step0 line 204
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1426 line 206
  52. def OAI.MUB6.Certificate.PairSemantics.raw1427 line 215
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1427 line 217
  54. def OAI.MUB6.Certificate.PairSemantics.raw1428 line 221
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1428 line 223
  56. def OAI.MUB6.Certificate.PairSemantics.raw1429 line 227
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1429 line 229
  58. def OAI.MUB6.Certificate.PairSemantics.raw1430 line 233
  59. def OAI.MUB6.Certificate.PairSemantics.raw1430step0 line 235
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1430 line 237
  61. def OAI.MUB6.Certificate.PairSemantics.raw1431 line 247
  62. def OAI.MUB6.Certificate.PairSemantics.raw1431step0 line 249
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1431 line 251
  64. def OAI.MUB6.Certificate.PairSemantics.raw1432 line 260
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1432 line 262
  66. def OAI.MUB6.Certificate.PairSemantics.raw1433 line 266
  67. def OAI.MUB6.Certificate.PairSemantics.raw1433step0 line 268
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1433 line 270
  69. def OAI.MUB6.Certificate.PairSemantics.raw1434 line 279
  70. def OAI.MUB6.Certificate.PairSemantics.raw1434step0 line 281
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1434 line 283
  72. def OAI.MUB6.Certificate.PairSemantics.raw1435 line 292
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1435 line 294
  74. def OAI.MUB6.Certificate.PairSemantics.raw1436 line 298
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1436 line 300
  76. def OAI.MUB6.Certificate.PairSemantics.raw1437 line 304
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1437 line 306
  78. def OAI.MUB6.Certificate.PairSemantics.raw1438 line 310
  79. def OAI.MUB6.Certificate.PairSemantics.raw1438step0 line 312
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1438 line 314
  81. def OAI.MUB6.Certificate.PairSemantics.raw1439 line 323
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1439 line 325