OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons76.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4864 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4864 line 12
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4865 line 33
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4865 line 35
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4866 line 56
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4866 line 58
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4868 line 79
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4868 line 81
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4869 line 102
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4869 line 104
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4871 line 125
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4871 line 127
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4874 line 148
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4874 line 150
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4875 line 171
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4875 line 173
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4887 line 194
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4887 line 196
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4888 line 217
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4888 line 219
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4889 line 240
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4889 line 242
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4890 line 263
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4890 line 265
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4896 line 286
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4896 line 288
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4898 line 309
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4898 line 311
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4899 line 332
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4899 line 334
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4902 line 355
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4902 line 357
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4903 line 378
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4903 line 380
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4904 line 401
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4904 line 403
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4905 line 424
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4905 line 426
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4906 line 447
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4906 line 449
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4907 line 470
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4907 line 472
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4908 line 493
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4908 line 495
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4909 line 516
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4909 line 518
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4910 line 539
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4910 line 541
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4912 line 562
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4912 line 564
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4913 line 585
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4913 line 587
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4914 line 608
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4914 line 610
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4917 line 631
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4917 line 633
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4919 line 654
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4919 line 656
  59. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4920 line 677
  60. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4920 line 679
  61. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4922 line 700
  62. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4922 line 702
  63. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4923 line 723
  64. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4923 line 725
  65. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4925 line 746
  66. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4925 line 748
  67. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4926 line 769
  68. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4926 line 771
  69. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4927 line 792
  70. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4927 line 794