OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons39.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall2526 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton2526 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall2527 line 27
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton2527 line 29
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall2528 line 45
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton2528 line 47
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall2530 line 63
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton2530 line 65
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall2531 line 81
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton2531 line 83
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall2532 line 99
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton2532 line 101