OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons48.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3081 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3081 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3082 line 28
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3082 line 30
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3087 line 46
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3087 line 48
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3088 line 64
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3088 line 66
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3089 line 82
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3089 line 84
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3090 line 100
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3090 line 102
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3093 line 118
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3093 line 120
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3094 line 136
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3094 line 138
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3095 line 154
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3095 line 156
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3099 line 172
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3099 line 174
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3100 line 190
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3100 line 192
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3101 line 208
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3101 line 210
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3102 line 226
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3102 line 228
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3103 line 244
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3103 line 246
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3105 line 262
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3105 line 264
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3106 line 280
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3106 line 282
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3109 line 298
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3109 line 300
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3110 line 316
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3110 line 318
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3113 line 334
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3113 line 336
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3116 line 352
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3116 line 354
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3117 line 370
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3117 line 372
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3119 line 388
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3119 line 390
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3120 line 406
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3120 line 408
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3121 line 424
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3121 line 426
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3125 line 442
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3125 line 444