OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons22.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1409 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1409 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1410 line 28
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1410 line 30
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1411 line 46
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1411 line 48
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1412 line 64
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1412 line 66
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1413 line 82
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1413 line 84
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1414 line 100
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1414 line 102
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1416 line 118
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1416 line 120
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1417 line 136
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1417 line 138
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1419 line 154
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1419 line 156
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1420 line 172
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1420 line 174
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1426 line 190
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1426 line 192
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1427 line 208
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1427 line 210
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1429 line 226
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1429 line 228
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1430 line 244
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1430 line 246
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1441 line 262
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1441 line 264
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1442 line 280
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1442 line 282
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1443 line 298
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1443 line 300
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1444 line 316
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1444 line 318
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1445 line 334
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1445 line 336
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1449 line 352
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1449 line 354
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1451 line 370
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1451 line 372
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1453 line 388
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1453 line 390
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1454 line 406
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1454 line 408
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1468 line 424
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1468 line 426
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1469 line 442
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1469 line 444
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1470 line 460
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1470 line 462
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall1471 line 478
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton1471 line 480