OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons10.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall644 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton644 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall645 line 27
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton645 line 29
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall646 line 45
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton646 line 47
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall647 line 63
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton647 line 65
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall648 line 81
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton648 line 83
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall649 line 99
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton649 line 101
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall650 line 117
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton650 line 119
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall652 line 135
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton652 line 137
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall655 line 153
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton655 line 155