OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical29.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw928 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw928step0 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw928step1 line 15
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical928 line 17
  5. def OAI.MUB6.Certificate.PairSemantics.raw929 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw929step0 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw929step1 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical929 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw930 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw930step0 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw930step1 line 53
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical930 line 55
  13. def OAI.MUB6.Certificate.PairSemantics.raw931 line 68
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical931 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw932 line 74
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical932 line 76
  17. def OAI.MUB6.Certificate.PairSemantics.raw933 line 80
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical933 line 82
  19. def OAI.MUB6.Certificate.PairSemantics.raw934 line 86
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical934 line 88
  21. def OAI.MUB6.Certificate.PairSemantics.raw935 line 92
  22. def OAI.MUB6.Certificate.PairSemantics.raw935step0 line 94
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical935 line 96
  24. def OAI.MUB6.Certificate.PairSemantics.raw936 line 105
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical936 line 107
  26. def OAI.MUB6.Certificate.PairSemantics.raw937 line 111
  27. def OAI.MUB6.Certificate.PairSemantics.raw937step0 line 113
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical937 line 115
  29. def OAI.MUB6.Certificate.PairSemantics.raw938 line 124
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical938 line 126
  31. def OAI.MUB6.Certificate.PairSemantics.raw939 line 130
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical939 line 132
  33. def OAI.MUB6.Certificate.PairSemantics.raw940 line 136
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical940 line 138
  35. def OAI.MUB6.Certificate.PairSemantics.raw941 line 142
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical941 line 144
  37. def OAI.MUB6.Certificate.PairSemantics.raw942 line 148
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical942 line 150
  39. def OAI.MUB6.Certificate.PairSemantics.raw943 line 154
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical943 line 156
  41. def OAI.MUB6.Certificate.PairSemantics.raw944 line 160
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical944 line 162
  43. def OAI.MUB6.Certificate.PairSemantics.raw945 line 166
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical945 line 168
  45. def OAI.MUB6.Certificate.PairSemantics.raw946 line 172
  46. def OAI.MUB6.Certificate.PairSemantics.raw946step0 line 174
  47. def OAI.MUB6.Certificate.PairSemantics.raw946step1 line 176
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical946 line 178
  49. def OAI.MUB6.Certificate.PairSemantics.raw947 line 191
  50. def OAI.MUB6.Certificate.PairSemantics.raw947step0 line 193
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical947 line 195
  52. def OAI.MUB6.Certificate.PairSemantics.raw948 line 204
  53. def OAI.MUB6.Certificate.PairSemantics.raw948step0 line 206
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical948 line 208
  55. def OAI.MUB6.Certificate.PairSemantics.raw949 line 217
  56. def OAI.MUB6.Certificate.PairSemantics.raw949step0 line 219
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical949 line 221
  58. def OAI.MUB6.Certificate.PairSemantics.raw950 line 230
  59. def OAI.MUB6.Certificate.PairSemantics.raw950step0 line 232
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical950 line 234
  61. def OAI.MUB6.Certificate.PairSemantics.raw951 line 243
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical951 line 245
  63. def OAI.MUB6.Certificate.PairSemantics.raw952 line 249
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical952 line 251
  65. def OAI.MUB6.Certificate.PairSemantics.raw953 line 255
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical953 line 257
  67. def OAI.MUB6.Certificate.PairSemantics.raw954 line 261
  68. def OAI.MUB6.Certificate.PairSemantics.raw954step0 line 263
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical954 line 265
  70. def OAI.MUB6.Certificate.PairSemantics.raw955 line 274
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical955 line 276
  72. def OAI.MUB6.Certificate.PairSemantics.raw956 line 280
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical956 line 282
  74. def OAI.MUB6.Certificate.PairSemantics.raw957 line 286
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical957 line 288
  76. def OAI.MUB6.Certificate.PairSemantics.raw958 line 292
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical958 line 294
  78. def OAI.MUB6.Certificate.PairSemantics.raw959 line 298
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical959 line 300