OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical62.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1984 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1984 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1985 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1985 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1986 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw1986step0 line 30
  7. def OAI.MUB6.Certificate.PairSemantics.raw1986step1 line 32
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1986 line 34
  9. def OAI.MUB6.Certificate.PairSemantics.raw1987 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw1987step0 line 49
  11. def OAI.MUB6.Certificate.PairSemantics.raw1987step1 line 51
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1987 line 53
  13. def OAI.MUB6.Certificate.PairSemantics.raw1988 line 66
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1988 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw1989 line 72
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1989 line 74
  17. def OAI.MUB6.Certificate.PairSemantics.raw1990 line 78
  18. def OAI.MUB6.Certificate.PairSemantics.raw1990step0 line 80
  19. def OAI.MUB6.Certificate.PairSemantics.raw1990step1 line 82
  20. def OAI.MUB6.Certificate.PairSemantics.raw1990step2 line 84
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1990 line 86
  22. def OAI.MUB6.Certificate.PairSemantics.raw1991 line 103
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1991 line 105
  24. def OAI.MUB6.Certificate.PairSemantics.raw1992 line 109
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1992 line 111
  26. def OAI.MUB6.Certificate.PairSemantics.raw1993 line 115
  27. def OAI.MUB6.Certificate.PairSemantics.raw1993step0 line 117
  28. def OAI.MUB6.Certificate.PairSemantics.raw1993step1 line 119
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1993 line 121
  30. def OAI.MUB6.Certificate.PairSemantics.raw1994 line 134
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1994 line 136
  32. def OAI.MUB6.Certificate.PairSemantics.raw1995 line 140
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1995 line 142
  34. def OAI.MUB6.Certificate.PairSemantics.raw1996 line 146
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1996 line 148
  36. def OAI.MUB6.Certificate.PairSemantics.raw1997 line 152
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1997 line 154
  38. def OAI.MUB6.Certificate.PairSemantics.raw1998 line 158
  39. def OAI.MUB6.Certificate.PairSemantics.raw1998step0 line 160
  40. def OAI.MUB6.Certificate.PairSemantics.raw1998step1 line 162
  41. def OAI.MUB6.Certificate.PairSemantics.raw1998step2 line 164
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1998 line 166
  43. def OAI.MUB6.Certificate.PairSemantics.raw1999 line 183
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1999 line 185
  45. def OAI.MUB6.Certificate.PairSemantics.raw2000 line 189
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2000 line 191
  47. def OAI.MUB6.Certificate.PairSemantics.raw2001 line 195
  48. def OAI.MUB6.Certificate.PairSemantics.raw2001step0 line 197
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2001 line 199
  50. def OAI.MUB6.Certificate.PairSemantics.raw2002 line 208
  51. def OAI.MUB6.Certificate.PairSemantics.raw2002step0 line 210
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2002 line 212
  53. def OAI.MUB6.Certificate.PairSemantics.raw2003 line 221
  54. def OAI.MUB6.Certificate.PairSemantics.raw2003step0 line 223
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2003 line 225
  56. def OAI.MUB6.Certificate.PairSemantics.raw2004 line 234
  57. def OAI.MUB6.Certificate.PairSemantics.raw2004step0 line 236
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical2004 line 238
  59. def OAI.MUB6.Certificate.PairSemantics.raw2005 line 247
  60. def OAI.MUB6.Certificate.PairSemantics.raw2005step0 line 249
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2005 line 251
  62. def OAI.MUB6.Certificate.PairSemantics.raw2006 line 260
  63. def OAI.MUB6.Certificate.PairSemantics.raw2006step0 line 262
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2006 line 264
  65. def OAI.MUB6.Certificate.PairSemantics.raw2007 line 273
  66. def OAI.MUB6.Certificate.PairSemantics.raw2007step0 line 275
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2007 line 277
  68. def OAI.MUB6.Certificate.PairSemantics.raw2008 line 286
  69. def OAI.MUB6.Certificate.PairSemantics.raw2008step0 line 288
  70. def OAI.MUB6.Certificate.PairSemantics.raw2008step1 line 290
  71. def OAI.MUB6.Certificate.PairSemantics.raw2008step2 line 292
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2008 line 294
  73. def OAI.MUB6.Certificate.PairSemantics.raw2009 line 312
  74. def OAI.MUB6.Certificate.PairSemantics.raw2009step0 line 314
  75. def OAI.MUB6.Certificate.PairSemantics.raw2009step1 line 316
  76. def OAI.MUB6.Certificate.PairSemantics.raw2009step2 line 318
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical2009 line 320
  78. def OAI.MUB6.Certificate.PairSemantics.raw2010 line 338
  79. def OAI.MUB6.Certificate.PairSemantics.raw2010step0 line 340
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical2010 line 342
  81. def OAI.MUB6.Certificate.PairSemantics.raw2011 line 351
  82. def OAI.MUB6.Certificate.PairSemantics.raw2011step0 line 353
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2011 line 355
  84. def OAI.MUB6.Certificate.PairSemantics.raw2012 line 364
  85. def OAI.MUB6.Certificate.PairSemantics.raw2012step0 line 366
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2012 line 368
  87. def OAI.MUB6.Certificate.PairSemantics.raw2013 line 377
  88. def OAI.MUB6.Certificate.PairSemantics.raw2013step0 line 379
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2013 line 381
  90. def OAI.MUB6.Certificate.PairSemantics.raw2014 line 390
  91. def OAI.MUB6.Certificate.PairSemantics.raw2014step0 line 392
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2014 line 394
  93. def OAI.MUB6.Certificate.PairSemantics.raw2015 line 403
  94. def OAI.MUB6.Certificate.PairSemantics.raw2015step0 line 405
  95. def OAI.MUB6.Certificate.PairSemantics.raw2015step1 line 407
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical2015 line 409