OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical153.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw4896 line 11
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical4896 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw4897 line 17
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical4897 line 19
  5. def OAI.MUB6.Certificate.PairSemantics.raw4898 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw4898step0 line 25
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical4898 line 27
  8. def OAI.MUB6.Certificate.PairSemantics.raw4899 line 36
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical4899 line 38
  10. def OAI.MUB6.Certificate.PairSemantics.raw4900 line 42
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical4900 line 44
  12. def OAI.MUB6.Certificate.PairSemantics.raw4901 line 48
  13. def OAI.MUB6.Certificate.PairSemantics.raw4901step0 line 50
  14. def OAI.MUB6.Certificate.PairSemantics.raw4901step1 line 52
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical4901 line 54
  16. def OAI.MUB6.Certificate.PairSemantics.raw4902 line 67
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical4902 line 69
  18. def OAI.MUB6.Certificate.PairSemantics.raw4903 line 73
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical4903 line 75
  20. def OAI.MUB6.Certificate.PairSemantics.raw4904 line 79
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical4904 line 81
  22. def OAI.MUB6.Certificate.PairSemantics.raw4905 line 85
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical4905 line 87
  24. def OAI.MUB6.Certificate.PairSemantics.raw4906 line 91
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical4906 line 93
  26. def OAI.MUB6.Certificate.PairSemantics.raw4907 line 97
  27. def OAI.MUB6.Certificate.PairSemantics.raw4907step0 line 99
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical4907 line 101
  29. def OAI.MUB6.Certificate.PairSemantics.raw4908 line 110
  30. def OAI.MUB6.Certificate.PairSemantics.raw4908step0 line 112
  31. def OAI.MUB6.Certificate.PairSemantics.raw4908step1 line 114
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical4908 line 116
  33. def OAI.MUB6.Certificate.PairSemantics.raw4909 line 129
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical4909 line 131
  35. def OAI.MUB6.Certificate.PairSemantics.raw4910 line 135
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical4910 line 137
  37. def OAI.MUB6.Certificate.PairSemantics.raw4911 line 141
  38. def OAI.MUB6.Certificate.PairSemantics.raw4911step0 line 143
  39. def OAI.MUB6.Certificate.PairSemantics.raw4911step1 line 145
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical4911 line 147
  41. def OAI.MUB6.Certificate.PairSemantics.raw4912 line 161
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical4912 line 163
  43. def OAI.MUB6.Certificate.PairSemantics.raw4913 line 167
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical4913 line 169
  45. def OAI.MUB6.Certificate.PairSemantics.raw4914 line 173
  46. def OAI.MUB6.Certificate.PairSemantics.raw4914step0 line 175
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical4914 line 177
  48. def OAI.MUB6.Certificate.PairSemantics.raw4915 line 186
  49. def OAI.MUB6.Certificate.PairSemantics.raw4915step0 line 188
  50. def OAI.MUB6.Certificate.PairSemantics.raw4915step1 line 190
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical4915 line 192
  52. def OAI.MUB6.Certificate.PairSemantics.raw4916 line 205
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical4916 line 207
  54. def OAI.MUB6.Certificate.PairSemantics.raw4917 line 211
  55. def OAI.MUB6.Certificate.PairSemantics.raw4917step0 line 213
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical4917 line 215
  57. def OAI.MUB6.Certificate.PairSemantics.raw4918 line 224
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical4918 line 226
  59. def OAI.MUB6.Certificate.PairSemantics.raw4919 line 230
  60. def OAI.MUB6.Certificate.PairSemantics.raw4919step0 line 232
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical4919 line 234
  62. def OAI.MUB6.Certificate.PairSemantics.raw4920 line 243
  63. def OAI.MUB6.Certificate.PairSemantics.raw4920step0 line 245
  64. def OAI.MUB6.Certificate.PairSemantics.raw4920step1 line 247
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical4920 line 249
  66. def OAI.MUB6.Certificate.PairSemantics.raw4921 line 262
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical4921 line 264
  68. def OAI.MUB6.Certificate.PairSemantics.raw4922 line 268
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical4922 line 270
  70. def OAI.MUB6.Certificate.PairSemantics.raw4923 line 274
  71. def OAI.MUB6.Certificate.PairSemantics.raw4923step0 line 276
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical4923 line 278
  73. def OAI.MUB6.Certificate.PairSemantics.raw4924 line 287
  74. def OAI.MUB6.Certificate.PairSemantics.raw4924step0 line 289
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical4924 line 291
  76. def OAI.MUB6.Certificate.PairSemantics.raw4925 line 300
  77. def OAI.MUB6.Certificate.PairSemantics.raw4925step0 line 302
  78. def OAI.MUB6.Certificate.PairSemantics.raw4925step1 line 304
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical4925 line 306
  80. def OAI.MUB6.Certificate.PairSemantics.raw4926 line 319
  81. def OAI.MUB6.Certificate.PairSemantics.raw4926step0 line 321
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical4926 line 323
  83. def OAI.MUB6.Certificate.PairSemantics.raw4927 line 332
  84. def OAI.MUB6.Certificate.PairSemantics.raw4927step0 line 334
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical4927 line 336