OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical43.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1376 line 10
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1376 line 12
  3. def OAI.MUB6.Certificate.PairSemantics.raw1377 line 16
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1377 line 18
  5. def OAI.MUB6.Certificate.PairSemantics.raw1378 line 22
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1378 line 24
  7. def OAI.MUB6.Certificate.PairSemantics.raw1379 line 28
  8. def OAI.MUB6.Certificate.PairSemantics.raw1379step0 line 30
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1379 line 32
  10. def OAI.MUB6.Certificate.PairSemantics.raw1380 line 42
  11. def OAI.MUB6.Certificate.PairSemantics.raw1380step0 line 44
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1380 line 46
  13. def OAI.MUB6.Certificate.PairSemantics.raw1381 line 56
  14. def OAI.MUB6.Certificate.PairSemantics.raw1381step0 line 58
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1381 line 60
  16. def OAI.MUB6.Certificate.PairSemantics.raw1382 line 70
  17. def OAI.MUB6.Certificate.PairSemantics.raw1382step0 line 72
  18. def OAI.MUB6.Certificate.PairSemantics.raw1382step1 line 74
  19. def OAI.MUB6.Certificate.PairSemantics.raw1382step2 line 76
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1382 line 78
  21. def OAI.MUB6.Certificate.PairSemantics.raw1383 line 96
  22. def OAI.MUB6.Certificate.PairSemantics.raw1383step0 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw1383step1 line 100
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1383 line 102
  25. def OAI.MUB6.Certificate.PairSemantics.raw1384 line 116
  26. def OAI.MUB6.Certificate.PairSemantics.raw1384step0 line 118
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1384 line 120
  28. def OAI.MUB6.Certificate.PairSemantics.raw1385 line 130
  29. def OAI.MUB6.Certificate.PairSemantics.raw1385step0 line 132
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1385 line 134
  31. def OAI.MUB6.Certificate.PairSemantics.raw1386 line 144
  32. def OAI.MUB6.Certificate.PairSemantics.raw1386step0 line 146
  33. def OAI.MUB6.Certificate.PairSemantics.raw1386step1 line 148
  34. def OAI.MUB6.Certificate.PairSemantics.raw1386step2 line 150
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1386 line 152
  36. def OAI.MUB6.Certificate.PairSemantics.raw1387 line 170
  37. def OAI.MUB6.Certificate.PairSemantics.raw1387step0 line 172
  38. def OAI.MUB6.Certificate.PairSemantics.raw1387step1 line 174
  39. def OAI.MUB6.Certificate.PairSemantics.raw1387step2 line 176
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1387 line 178
  41. def OAI.MUB6.Certificate.PairSemantics.raw1388 line 196
  42. def OAI.MUB6.Certificate.PairSemantics.raw1388step0 line 198
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1388 line 200
  44. def OAI.MUB6.Certificate.PairSemantics.raw1389 line 210
  45. def OAI.MUB6.Certificate.PairSemantics.raw1389step0 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw1389step1 line 214
  47. def OAI.MUB6.Certificate.PairSemantics.raw1389step2 line 216
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1389 line 218
  49. def OAI.MUB6.Certificate.PairSemantics.raw1390 line 236
  50. def OAI.MUB6.Certificate.PairSemantics.raw1390step0 line 238
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1390 line 240
  52. def OAI.MUB6.Certificate.PairSemantics.raw1391 line 249
  53. def OAI.MUB6.Certificate.PairSemantics.raw1391step0 line 251
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical1391 line 253
  55. def OAI.MUB6.Certificate.PairSemantics.raw1392 line 262
  56. def OAI.MUB6.Certificate.PairSemantics.raw1392step0 line 264
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1392 line 266
  58. def OAI.MUB6.Certificate.PairSemantics.raw1393 line 275
  59. def OAI.MUB6.Certificate.PairSemantics.raw1393step0 line 277
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1393 line 279
  61. def OAI.MUB6.Certificate.PairSemantics.raw1394 line 289
  62. def OAI.MUB6.Certificate.PairSemantics.raw1394step0 line 291
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1394 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw1395 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw1395step0 line 305
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1395 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw1396 line 317
  68. def OAI.MUB6.Certificate.PairSemantics.raw1396step0 line 319
  69. def OAI.MUB6.Certificate.PairSemantics.raw1396step1 line 321
  70. def OAI.MUB6.Certificate.PairSemantics.raw1396step2 line 323
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1396 line 325
  72. def OAI.MUB6.Certificate.PairSemantics.raw1397 line 343
  73. def OAI.MUB6.Certificate.PairSemantics.raw1397step0 line 345
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1397 line 347
  75. def OAI.MUB6.Certificate.PairSemantics.raw1398 line 357
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1398 line 359
  77. def OAI.MUB6.Certificate.PairSemantics.raw1399 line 363
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1399 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw1400 line 369
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1400 line 371
  81. def OAI.MUB6.Certificate.PairSemantics.raw1401 line 375
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1401 line 377
  83. def OAI.MUB6.Certificate.PairSemantics.raw1402 line 381
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical1402 line 383
  85. def OAI.MUB6.Certificate.PairSemantics.raw1403 line 387
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1403 line 389
  87. def OAI.MUB6.Certificate.PairSemantics.raw1404 line 393
  88. def OAI.MUB6.Certificate.PairSemantics.raw1404step0 line 395
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1404 line 397
  90. def OAI.MUB6.Certificate.PairSemantics.raw1405 line 406
  91. def OAI.MUB6.Certificate.PairSemantics.raw1405step0 line 408
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1405 line 410
  93. def OAI.MUB6.Certificate.PairSemantics.raw1406 line 420
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical1406 line 422
  95. def OAI.MUB6.Certificate.PairSemantics.raw1407 line 426
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1407 line 428