OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical30.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw960 line 15
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical960 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw961 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw961step0 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw961step1 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical961 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw962 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw962step0 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw962step1 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical962 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw963 line 59
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical963 line 61
  13. def OAI.MUB6.Certificate.PairSemantics.raw964 line 65
  14. def OAI.MUB6.Certificate.PairSemantics.raw964step0 line 67
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical964 line 69
  16. def OAI.MUB6.Certificate.PairSemantics.raw965 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw965step0 line 80
  18. def OAI.MUB6.Certificate.PairSemantics.raw965step1 line 82
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical965 line 84
  20. def OAI.MUB6.Certificate.PairSemantics.raw966 line 97
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical966 line 99
  22. def OAI.MUB6.Certificate.PairSemantics.raw967 line 103
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical967 line 105
  24. def OAI.MUB6.Certificate.PairSemantics.raw968 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw968step0 line 111
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical968 line 113
  27. def OAI.MUB6.Certificate.PairSemantics.raw969 line 122
  28. def OAI.MUB6.Certificate.PairSemantics.raw969step0 line 124
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical969 line 126
  30. def OAI.MUB6.Certificate.PairSemantics.raw970 line 135
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical970 line 137
  32. def OAI.MUB6.Certificate.PairSemantics.raw971 line 141
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical971 line 143
  34. def OAI.MUB6.Certificate.PairSemantics.raw972 line 147
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical972 line 149
  36. def OAI.MUB6.Certificate.PairSemantics.raw973 line 153
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical973 line 155
  38. def OAI.MUB6.Certificate.PairSemantics.raw974 line 159
  39. def OAI.MUB6.Certificate.PairSemantics.raw974step0 line 161
  40. def OAI.MUB6.Certificate.PairSemantics.raw974step1 line 163
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical974 line 165
  42. def OAI.MUB6.Certificate.PairSemantics.raw975 line 178
  43. def OAI.MUB6.Certificate.PairSemantics.raw975step0 line 180
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical975 line 182
  45. def OAI.MUB6.Certificate.PairSemantics.raw976 line 191
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical976 line 193
  47. def OAI.MUB6.Certificate.PairSemantics.raw977 line 197
  48. def OAI.MUB6.Certificate.PairSemantics.raw977step0 line 199
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical977 line 201
  50. def OAI.MUB6.Certificate.PairSemantics.raw978 line 210
  51. def OAI.MUB6.Certificate.PairSemantics.raw978step0 line 212
  52. def OAI.MUB6.Certificate.PairSemantics.raw978step1 line 214
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical978 line 216
  54. def OAI.MUB6.Certificate.PairSemantics.raw979 line 229
  55. def OAI.MUB6.Certificate.PairSemantics.raw979step0 line 231
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical979 line 233
  57. def OAI.MUB6.Certificate.PairSemantics.raw980 line 242
  58. def OAI.MUB6.Certificate.PairSemantics.raw980step0 line 244
  59. def OAI.MUB6.Certificate.PairSemantics.raw980step1 line 246
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical980 line 248
  61. def OAI.MUB6.Certificate.PairSemantics.raw981 line 261
  62. def OAI.MUB6.Certificate.PairSemantics.raw981step0 line 263
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical981 line 265
  64. def OAI.MUB6.Certificate.PairSemantics.raw982 line 274
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical982 line 276
  66. def OAI.MUB6.Certificate.PairSemantics.raw983 line 280
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical983 line 282
  68. def OAI.MUB6.Certificate.PairSemantics.raw984 line 286
  69. def OAI.MUB6.Certificate.PairSemantics.raw984step0 line 288
  70. def OAI.MUB6.Certificate.PairSemantics.raw984step1 line 290
  71. def OAI.MUB6.Certificate.PairSemantics.raw984step2 line 292
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical984 line 294
  73. def OAI.MUB6.Certificate.PairSemantics.raw985 line 311
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical985 line 313
  75. def OAI.MUB6.Certificate.PairSemantics.raw986 line 317
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical986 line 319
  77. def OAI.MUB6.Certificate.PairSemantics.raw987 line 323
  78. def OAI.MUB6.Certificate.PairSemantics.raw987step0 line 325
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical987 line 327
  80. def OAI.MUB6.Certificate.PairSemantics.raw988 line 336
  81. def OAI.MUB6.Certificate.PairSemantics.raw988step0 line 338
  82. def OAI.MUB6.Certificate.PairSemantics.raw988step1 line 340
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical988 line 342
  84. def OAI.MUB6.Certificate.PairSemantics.raw989 line 355
  85. def OAI.MUB6.Certificate.PairSemantics.raw989step0 line 357
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical989 line 359
  87. def OAI.MUB6.Certificate.PairSemantics.raw990 line 368
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical990 line 370
  89. def OAI.MUB6.Certificate.PairSemantics.raw991 line 374
  90. def OAI.MUB6.Certificate.PairSemantics.raw991step0 line 376
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical991 line 378