OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical90.lean

GitHub source file

102 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2880 line 17
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2880 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw2881 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2881 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw2882 line 29
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical2882 line 31
  7. def OAI.MUB6.Certificate.PairSemantics.raw2883 line 35
  8. def OAI.MUB6.Certificate.PairSemantics.raw2883step0 line 37
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2883 line 39
  10. def OAI.MUB6.Certificate.PairSemantics.raw2884 line 48
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2884 line 50
  12. def OAI.MUB6.Certificate.PairSemantics.raw2885 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw2885step0 line 56
  14. def OAI.MUB6.Certificate.PairSemantics.raw2885step1 line 58
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2885 line 60
  16. def OAI.MUB6.Certificate.PairSemantics.raw2886 line 73
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2886 line 75
  18. def OAI.MUB6.Certificate.PairSemantics.raw2887 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw2887step0 line 81
  20. def OAI.MUB6.Certificate.PairSemantics.raw2887step1 line 83
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2887 line 85
  22. def OAI.MUB6.Certificate.PairSemantics.raw2888 line 98
  23. def OAI.MUB6.Certificate.PairSemantics.raw2888step0 line 100
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2888 line 102
  25. def OAI.MUB6.Certificate.PairSemantics.raw2889 line 111
  26. def OAI.MUB6.Certificate.PairSemantics.raw2889step0 line 113
  27. def OAI.MUB6.Certificate.PairSemantics.raw2889step1 line 115
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2889 line 117
  29. def OAI.MUB6.Certificate.PairSemantics.raw2890 line 130
  30. def OAI.MUB6.Certificate.PairSemantics.raw2890step0 line 132
  31. def OAI.MUB6.Certificate.PairSemantics.raw2890step1 line 134
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2890 line 136
  33. def OAI.MUB6.Certificate.PairSemantics.raw2891 line 149
  34. def OAI.MUB6.Certificate.PairSemantics.raw2891step0 line 151
  35. def OAI.MUB6.Certificate.PairSemantics.raw2891step1 line 153
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2891 line 155
  37. def OAI.MUB6.Certificate.PairSemantics.raw2892 line 168
  38. def OAI.MUB6.Certificate.PairSemantics.raw2892step0 line 170
  39. def OAI.MUB6.Certificate.PairSemantics.raw2892step1 line 172
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2892 line 174
  41. def OAI.MUB6.Certificate.PairSemantics.raw2893 line 187
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2893 line 189
  43. def OAI.MUB6.Certificate.PairSemantics.raw2894 line 193
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2894 line 195
  45. def OAI.MUB6.Certificate.PairSemantics.raw2895 line 199
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2895 line 201
  47. def OAI.MUB6.Certificate.PairSemantics.raw2896 line 205
  48. def OAI.MUB6.Certificate.PairSemantics.raw2896step0 line 207
  49. def OAI.MUB6.Certificate.PairSemantics.raw2896step1 line 209
  50. def OAI.MUB6.Certificate.PairSemantics.raw2896step2 line 211
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical2896 line 213
  52. def OAI.MUB6.Certificate.PairSemantics.raw2897 line 231
  53. def OAI.MUB6.Certificate.PairSemantics.raw2897step0 line 233
  54. def OAI.MUB6.Certificate.PairSemantics.raw2897step1 line 235
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2897 line 237
  56. def OAI.MUB6.Certificate.PairSemantics.raw2898 line 250
  57. def OAI.MUB6.Certificate.PairSemantics.raw2898step0 line 252
  58. def OAI.MUB6.Certificate.PairSemantics.raw2898step1 line 254
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2898 line 256
  60. def OAI.MUB6.Certificate.PairSemantics.raw2899 line 269
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2899 line 271
  62. def OAI.MUB6.Certificate.PairSemantics.raw2900 line 275
  63. def OAI.MUB6.Certificate.PairSemantics.raw2900step0 line 277
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2900 line 279
  65. def OAI.MUB6.Certificate.PairSemantics.raw2901 line 288
  66. def OAI.MUB6.Certificate.PairSemantics.raw2901step0 line 290
  67. def OAI.MUB6.Certificate.PairSemantics.raw2901step1 line 292
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical2901 line 294
  69. def OAI.MUB6.Certificate.PairSemantics.raw2902 line 307
  70. def OAI.MUB6.Certificate.PairSemantics.raw2902step0 line 309
  71. def OAI.MUB6.Certificate.PairSemantics.raw2902step1 line 311
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2902 line 313
  73. def OAI.MUB6.Certificate.PairSemantics.raw2903 line 326
  74. def OAI.MUB6.Certificate.PairSemantics.raw2903step0 line 328
  75. def OAI.MUB6.Certificate.PairSemantics.raw2903step1 line 330
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2903 line 332
  77. def OAI.MUB6.Certificate.PairSemantics.raw2904 line 345
  78. def OAI.MUB6.Certificate.PairSemantics.raw2904step0 line 347
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2904 line 349
  80. def OAI.MUB6.Certificate.PairSemantics.raw2905 line 358
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical2905 line 360
  82. def OAI.MUB6.Certificate.PairSemantics.raw2906 line 364
  83. def OAI.MUB6.Certificate.PairSemantics.raw2906step0 line 366
  84. def OAI.MUB6.Certificate.PairSemantics.raw2906step1 line 368
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical2906 line 370
  86. def OAI.MUB6.Certificate.PairSemantics.raw2907 line 383
  87. def OAI.MUB6.Certificate.PairSemantics.raw2907step0 line 385
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2907 line 387
  89. def OAI.MUB6.Certificate.PairSemantics.raw2908 line 396
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2908 line 398
  91. def OAI.MUB6.Certificate.PairSemantics.raw2909 line 402
  92. def OAI.MUB6.Certificate.PairSemantics.raw2909step0 line 404
  93. def OAI.MUB6.Certificate.PairSemantics.raw2909step1 line 406
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2909 line 408
  95. def OAI.MUB6.Certificate.PairSemantics.raw2910 line 421
  96. def OAI.MUB6.Certificate.PairSemantics.raw2910step0 line 423
  97. def OAI.MUB6.Certificate.PairSemantics.raw2910step1 line 425
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical2910 line 427
  99. def OAI.MUB6.Certificate.PairSemantics.raw2911 line 440
  100. def OAI.MUB6.Certificate.PairSemantics.raw2911step0 line 442
  101. def OAI.MUB6.Certificate.PairSemantics.raw2911step1 line 444
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical2911 line 446