OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical45.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1440 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1440 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw1441 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1441 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw1442 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1442 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw1443 line 31
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1443 line 33
  9. def OAI.MUB6.Certificate.PairSemantics.raw1444 line 37
  10. def OAI.MUB6.Certificate.PairSemantics.raw1444step0 line 39
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1444 line 41
  12. def OAI.MUB6.Certificate.PairSemantics.raw1445 line 50
  13. def OAI.MUB6.Certificate.PairSemantics.raw1445step0 line 52
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1445 line 54
  15. def OAI.MUB6.Certificate.PairSemantics.raw1446 line 63
  16. def OAI.MUB6.Certificate.PairSemantics.raw1446step0 line 65
  17. def OAI.MUB6.Certificate.PairSemantics.raw1446step1 line 67
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1446 line 69
  19. def OAI.MUB6.Certificate.PairSemantics.raw1447 line 82
  20. def OAI.MUB6.Certificate.PairSemantics.raw1447step0 line 84
  21. def OAI.MUB6.Certificate.PairSemantics.raw1447step1 line 86
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1447 line 88
  23. def OAI.MUB6.Certificate.PairSemantics.raw1448 line 101
  24. def OAI.MUB6.Certificate.PairSemantics.raw1448step0 line 103
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1448 line 105
  26. def OAI.MUB6.Certificate.PairSemantics.raw1449 line 114
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1449 line 116
  28. def OAI.MUB6.Certificate.PairSemantics.raw1450 line 120
  29. def OAI.MUB6.Certificate.PairSemantics.raw1450step0 line 122
  30. def OAI.MUB6.Certificate.PairSemantics.raw1450step1 line 124
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1450 line 126
  32. def OAI.MUB6.Certificate.PairSemantics.raw1451 line 139
  33. def OAI.MUB6.Certificate.PairSemantics.raw1451step0 line 141
  34. def OAI.MUB6.Certificate.PairSemantics.raw1451step1 line 143
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1451 line 145
  36. def OAI.MUB6.Certificate.PairSemantics.raw1452 line 158
  37. def OAI.MUB6.Certificate.PairSemantics.raw1452step0 line 160
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1452 line 162
  39. def OAI.MUB6.Certificate.PairSemantics.raw1453 line 171
  40. def OAI.MUB6.Certificate.PairSemantics.raw1453step0 line 173
  41. def OAI.MUB6.Certificate.PairSemantics.raw1453step1 line 175
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1453 line 177
  43. def OAI.MUB6.Certificate.PairSemantics.raw1454 line 190
  44. def OAI.MUB6.Certificate.PairSemantics.raw1454step0 line 192
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1454 line 194
  46. def OAI.MUB6.Certificate.PairSemantics.raw1455 line 203
  47. def OAI.MUB6.Certificate.PairSemantics.raw1455step0 line 205
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1455 line 207
  49. def OAI.MUB6.Certificate.PairSemantics.raw1456 line 216
  50. def OAI.MUB6.Certificate.PairSemantics.raw1456step0 line 218
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1456 line 220
  52. def OAI.MUB6.Certificate.PairSemantics.raw1457 line 229
  53. def OAI.MUB6.Certificate.PairSemantics.raw1457step0 line 231
  54. def OAI.MUB6.Certificate.PairSemantics.raw1457step1 line 233
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1457 line 235
  56. def OAI.MUB6.Certificate.PairSemantics.raw1458 line 248
  57. def OAI.MUB6.Certificate.PairSemantics.raw1458step0 line 250
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1458 line 252
  59. def OAI.MUB6.Certificate.PairSemantics.raw1459 line 261
  60. def OAI.MUB6.Certificate.PairSemantics.raw1459step0 line 263
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1459 line 265
  62. def OAI.MUB6.Certificate.PairSemantics.raw1460 line 274
  63. def OAI.MUB6.Certificate.PairSemantics.raw1460step0 line 276
  64. def OAI.MUB6.Certificate.PairSemantics.raw1460step1 line 278
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1460 line 280
  66. def OAI.MUB6.Certificate.PairSemantics.raw1461 line 293
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1461 line 295
  68. def OAI.MUB6.Certificate.PairSemantics.raw1462 line 299
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1462 line 301
  70. def OAI.MUB6.Certificate.PairSemantics.raw1463 line 305
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1463 line 307
  72. def OAI.MUB6.Certificate.PairSemantics.raw1464 line 311
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1464 line 313
  74. def OAI.MUB6.Certificate.PairSemantics.raw1465 line 317
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1465 line 319
  76. def OAI.MUB6.Certificate.PairSemantics.raw1466 line 323
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1466 line 325
  78. def OAI.MUB6.Certificate.PairSemantics.raw1467 line 329
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical1467 line 331
  80. def OAI.MUB6.Certificate.PairSemantics.raw1468 line 335
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical1468 line 337
  82. def OAI.MUB6.Certificate.PairSemantics.raw1469 line 341
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1469 line 343
  84. def OAI.MUB6.Certificate.PairSemantics.raw1470 line 347
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1470 line 349
  86. def OAI.MUB6.Certificate.PairSemantics.raw1471 line 353
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1471 line 355