OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical42.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1344 line 12
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1344 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw1345 line 18
  4. def OAI.MUB6.Certificate.PairSemantics.raw1345step0 line 20
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1345 line 22
  6. def OAI.MUB6.Certificate.PairSemantics.raw1346 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw1346step0 line 33
  8. def OAI.MUB6.Certificate.PairSemantics.raw1346step1 line 35
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1346 line 37
  10. def OAI.MUB6.Certificate.PairSemantics.raw1347 line 50
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1347 line 52
  12. def OAI.MUB6.Certificate.PairSemantics.raw1348 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw1348step0 line 58
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1348 line 60
  15. def OAI.MUB6.Certificate.PairSemantics.raw1349 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw1349step0 line 71
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1349 line 73
  18. def OAI.MUB6.Certificate.PairSemantics.raw1350 line 82
  19. def OAI.MUB6.Certificate.PairSemantics.raw1350step0 line 84
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1350 line 86
  21. def OAI.MUB6.Certificate.PairSemantics.raw1351 line 95
  22. def OAI.MUB6.Certificate.PairSemantics.raw1351step0 line 97
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1351 line 99
  24. def OAI.MUB6.Certificate.PairSemantics.raw1352 line 108
  25. def OAI.MUB6.Certificate.PairSemantics.raw1352step0 line 110
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1352 line 112
  27. def OAI.MUB6.Certificate.PairSemantics.raw1353 line 121
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1353 line 123
  29. def OAI.MUB6.Certificate.PairSemantics.raw1354 line 127
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1354 line 129
  31. def OAI.MUB6.Certificate.PairSemantics.raw1355 line 133
  32. def OAI.MUB6.Certificate.PairSemantics.raw1355step0 line 135
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1355 line 137
  34. def OAI.MUB6.Certificate.PairSemantics.raw1356 line 146
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1356 line 148
  36. def OAI.MUB6.Certificate.PairSemantics.raw1357 line 152
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1357 line 154
  38. def OAI.MUB6.Certificate.PairSemantics.raw1358 line 158
  39. def OAI.MUB6.Certificate.PairSemantics.raw1358step0 line 160
  40. def OAI.MUB6.Certificate.PairSemantics.raw1358step1 line 162
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1358 line 164
  42. def OAI.MUB6.Certificate.PairSemantics.raw1359 line 177
  43. def OAI.MUB6.Certificate.PairSemantics.raw1359step0 line 179
  44. def OAI.MUB6.Certificate.PairSemantics.raw1359step1 line 181
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1359 line 183
  46. def OAI.MUB6.Certificate.PairSemantics.raw1360 line 196
  47. def OAI.MUB6.Certificate.PairSemantics.raw1360step0 line 198
  48. def OAI.MUB6.Certificate.PairSemantics.raw1360step1 line 200
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1360 line 202
  50. def OAI.MUB6.Certificate.PairSemantics.raw1361 line 215
  51. def OAI.MUB6.Certificate.PairSemantics.raw1361step0 line 217
  52. def OAI.MUB6.Certificate.PairSemantics.raw1361step1 line 219
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1361 line 221
  54. def OAI.MUB6.Certificate.PairSemantics.raw1362 line 234
  55. def OAI.MUB6.Certificate.PairSemantics.raw1362step0 line 236
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1362 line 238
  57. def OAI.MUB6.Certificate.PairSemantics.raw1363 line 247
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1363 line 249
  59. def OAI.MUB6.Certificate.PairSemantics.raw1364 line 253
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1364 line 255
  61. def OAI.MUB6.Certificate.PairSemantics.raw1365 line 259
  62. def OAI.MUB6.Certificate.PairSemantics.raw1365step0 line 261
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1365 line 263
  64. def OAI.MUB6.Certificate.PairSemantics.raw1366 line 272
  65. def OAI.MUB6.Certificate.PairSemantics.raw1366step0 line 274
  66. def OAI.MUB6.Certificate.PairSemantics.raw1366step1 line 276
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1366 line 278
  68. def OAI.MUB6.Certificate.PairSemantics.raw1367 line 291
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1367 line 293
  70. def OAI.MUB6.Certificate.PairSemantics.raw1368 line 297
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1368 line 299
  72. def OAI.MUB6.Certificate.PairSemantics.raw1369 line 303
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1369 line 305
  74. def OAI.MUB6.Certificate.PairSemantics.raw1370 line 309
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1370 line 311
  76. def OAI.MUB6.Certificate.PairSemantics.raw1371 line 315
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1371 line 317
  78. def OAI.MUB6.Certificate.PairSemantics.raw1372 line 321
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical1372 line 323
  80. def OAI.MUB6.Certificate.PairSemantics.raw1373 line 327
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical1373 line 329
  82. def OAI.MUB6.Certificate.PairSemantics.raw1374 line 333
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1374 line 335
  84. def OAI.MUB6.Certificate.PairSemantics.raw1375 line 339
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1375 line 341