OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons81.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5192 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5192 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5193 line 32
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5193 line 34
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5202 line 55
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5202 line 57
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5203 line 78
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5203 line 80
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5204 line 101
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5204 line 103
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5207 line 124
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5207 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5212 line 147
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5212 line 149
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5213 line 170
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5213 line 172
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5214 line 193
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5214 line 195
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5227 line 216
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5227 line 218
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5228 line 239
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5228 line 241
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5237 line 262
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5237 line 264
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5238 line 285
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5238 line 287
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5241 line 308
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5241 line 310
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall5247 line 331
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton5247 line 333