OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical32.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1024 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw1024step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw1024step1 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1024 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw1025 line 36
  6. def OAI.MUB6.Certificate.PairSemantics.raw1025step0 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw1025step1 line 40
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1025 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw1026 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw1026step0 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw1026step1 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1026 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw1027 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw1027step0 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw1027step1 line 78
  16. def OAI.MUB6.Certificate.PairSemantics.raw1027step2 line 80
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1027 line 82
  18. def OAI.MUB6.Certificate.PairSemantics.raw1028 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw1028step0 line 101
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical1028 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw1029 line 112
  22. def OAI.MUB6.Certificate.PairSemantics.raw1029step0 line 114
  23. def OAI.MUB6.Certificate.PairSemantics.raw1029step1 line 116
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1029 line 118
  25. def OAI.MUB6.Certificate.PairSemantics.raw1030 line 131
  26. def OAI.MUB6.Certificate.PairSemantics.raw1030step0 line 133
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1030 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw1031 line 144
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1031 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw1032 line 150
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1032 line 152
  32. def OAI.MUB6.Certificate.PairSemantics.raw1033 line 156
  33. def OAI.MUB6.Certificate.PairSemantics.raw1033step0 line 158
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1033 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw1034 line 169
  36. def OAI.MUB6.Certificate.PairSemantics.raw1034step0 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw1034step1 line 173
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1034 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw1035 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw1035step0 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw1035step1 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw1035step2 line 194
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1035 line 196
  44. def OAI.MUB6.Certificate.PairSemantics.raw1036 line 214
  45. def OAI.MUB6.Certificate.PairSemantics.raw1036step0 line 216
  46. def OAI.MUB6.Certificate.PairSemantics.raw1036step1 line 218
  47. def OAI.MUB6.Certificate.PairSemantics.raw1036step2 line 220
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1036 line 222
  49. def OAI.MUB6.Certificate.PairSemantics.raw1037 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw1037step0 line 242
  51. def OAI.MUB6.Certificate.PairSemantics.raw1037step1 line 244
  52. def OAI.MUB6.Certificate.PairSemantics.raw1037step2 line 246
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1037 line 248
  54. def OAI.MUB6.Certificate.PairSemantics.raw1038 line 266
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1038 line 268
  56. def OAI.MUB6.Certificate.PairSemantics.raw1039 line 272
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1039 line 274
  58. def OAI.MUB6.Certificate.PairSemantics.raw1040 line 278
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1040 line 280
  60. def OAI.MUB6.Certificate.PairSemantics.raw1041 line 284
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1041 line 286
  62. def OAI.MUB6.Certificate.PairSemantics.raw1042 line 290
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1042 line 292
  64. def OAI.MUB6.Certificate.PairSemantics.raw1043 line 296
  65. def OAI.MUB6.Certificate.PairSemantics.raw1043step0 line 298
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1043 line 300
  67. def OAI.MUB6.Certificate.PairSemantics.raw1044 line 309
  68. def OAI.MUB6.Certificate.PairSemantics.raw1044step0 line 311
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1044 line 313
  70. def OAI.MUB6.Certificate.PairSemantics.raw1045 line 322
  71. def OAI.MUB6.Certificate.PairSemantics.raw1045step0 line 324
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1045 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw1046 line 335
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1046 line 337
  75. def OAI.MUB6.Certificate.PairSemantics.raw1047 line 341
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1047 line 343
  77. def OAI.MUB6.Certificate.PairSemantics.raw1048 line 347
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1048 line 349
  79. def OAI.MUB6.Certificate.PairSemantics.raw1049 line 353
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1049 line 355
  81. def OAI.MUB6.Certificate.PairSemantics.raw1050 line 359
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1050 line 361
  83. def OAI.MUB6.Certificate.PairSemantics.raw1051 line 365
  84. def OAI.MUB6.Certificate.PairSemantics.raw1051step0 line 367
  85. def OAI.MUB6.Certificate.PairSemantics.raw1051step1 line 369
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1051 line 371
  87. def OAI.MUB6.Certificate.PairSemantics.raw1052 line 384
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical1052 line 386
  89. def OAI.MUB6.Certificate.PairSemantics.raw1053 line 390
  90. def OAI.MUB6.Certificate.PairSemantics.raw1053step0 line 392
  91. def OAI.MUB6.Certificate.PairSemantics.raw1053step1 line 394
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1053 line 396
  93. def OAI.MUB6.Certificate.PairSemantics.raw1054 line 409
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical1054 line 411
  95. def OAI.MUB6.Certificate.PairSemantics.raw1055 line 415
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical1055 line 417