OAI/Analysis/MutuallyUnbiased/MixedMerge/Block62.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1984 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1984 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1984 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1985 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1985 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1985 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1986 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1986 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1986 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged1987 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1987 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1987 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1988 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1988 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1988 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged1989 line 55
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1989 line 57
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1989 line 59
  19. def OAI.MUB6.Certificate.MixedData.merged1990 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1990 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1990 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged1991 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1991 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1991 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1992 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1992 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1992 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1993 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1993 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1993 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged1994 line 103
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1994 line 105
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1994 line 107
  34. def OAI.MUB6.Certificate.MixedData.merged1995 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1995 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1995 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged1996 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1996 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1996 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1997 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1997 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1997 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged1998 line 141
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1998 line 143
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1998 line 145
  46. def OAI.MUB6.Certificate.MixedData.merged1999 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1999 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1999 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged2000 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2000 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2000 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged2001 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2001 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2001 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged2002part0 line 181
  56. def OAI.MUB6.Certificate.MixedData.merged2002part1 line 183
  57. def OAI.MUB6.Certificate.MixedData.merged2002part2 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2002part3 line 187
  59. def OAI.MUB6.Certificate.MixedData.merged2002part4 line 189
  60. def OAI.MUB6.Certificate.MixedData.merged2002part5 line 191
  61. def OAI.MUB6.Certificate.MixedData.merged2002part6 line 193
  62. def OAI.MUB6.Certificate.MixedData.merged2002part7 line 195
  63. def OAI.MUB6.Certificate.MixedData.merged2002part8 line 197
  64. def OAI.MUB6.Certificate.MixedData.merged2002 line 199
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2002 line 201
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2002 line 203
  67. def OAI.MUB6.Certificate.MixedData.merged2003 line 209
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2003 line 211
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2003 line 213
  70. def OAI.MUB6.Certificate.MixedData.merged2004 line 218
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2004 line 220
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2004 line 222
  73. def OAI.MUB6.Certificate.MixedData.merged2005 line 227
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2005 line 229
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2005 line 231
  76. def OAI.MUB6.Certificate.MixedData.merged2006 line 237
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2006 line 239
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2006 line 241
  79. def OAI.MUB6.Certificate.MixedData.merged2007 line 246
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2007 line 248
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2007 line 250
  82. def OAI.MUB6.Certificate.MixedData.merged2008 line 255
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2008 line 257
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2008 line 259
  85. def OAI.MUB6.Certificate.MixedData.merged2009 line 265
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2009 line 267
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2009 line 269
  88. def OAI.MUB6.Certificate.MixedData.merged2010 line 275
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2010 line 277
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2010 line 279
  91. def OAI.MUB6.Certificate.MixedData.merged2011 line 285
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2011 line 287
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2011 line 289
  94. def OAI.MUB6.Certificate.MixedData.merged2012 line 294
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2012 line 296
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2012 line 298
  97. def OAI.MUB6.Certificate.MixedData.merged2013 line 303
  98. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2013 line 305
  99. theorem OAI.MUB6.Certificate.MixedData.mergedZero2013 line 307
  100. def OAI.MUB6.Certificate.MixedData.merged2014 line 313
  101. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2014 line 315
  102. theorem OAI.MUB6.Certificate.MixedData.mergedZero2014 line 317
  103. def OAI.MUB6.Certificate.MixedData.merged2015 line 323
  104. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2015 line 325
  105. theorem OAI.MUB6.Certificate.MixedData.mergedZero2015 line 327