OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons59.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3818 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3818 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3820 line 28
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3820 line 30
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3821 line 46
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3821 line 48
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3822 line 64
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3822 line 66
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3823 line 82
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3823 line 84
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3824 line 100
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3824 line 102
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3829 line 118
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3829 line 120
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3830 line 136
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3830 line 138
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall3831 line 154
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton3831 line 156