OAI/Analysis/MutuallyUnbiased/MixedSemantics/Singletons67.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4288 line 9
  2. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4288 line 11
  3. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4289 line 32
  4. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4289 line 34
  5. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4290 line 55
  6. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4290 line 57
  7. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4291 line 78
  8. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4291 line 80
  9. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4292 line 101
  10. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4292 line 103
  11. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4293 line 124
  12. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4293 line 126
  13. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4294 line 147
  14. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4294 line 149
  15. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4295 line 170
  16. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4295 line 172
  17. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4296 line 193
  18. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4296 line 195
  19. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4297 line 216
  20. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4297 line 218
  21. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4298 line 239
  22. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4298 line 241
  23. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4299 line 262
  24. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4299 line 264
  25. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4301 line 285
  26. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4301 line 287
  27. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4303 line 308
  28. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4303 line 310
  29. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4304 line 331
  30. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4304 line 333
  31. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4307 line 354
  32. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4307 line 356
  33. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4309 line 377
  34. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4309 line 379
  35. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4310 line 400
  36. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4310 line 402
  37. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4313 line 423
  38. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4313 line 425
  39. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4314 line 446
  40. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4314 line 448
  41. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4315 line 469
  42. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4315 line 471
  43. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4316 line 492
  44. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4316 line 494
  45. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4319 line 515
  46. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4319 line 517
  47. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4320 line 538
  48. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4320 line 540
  49. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4321 line 561
  50. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4321 line 563
  51. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4322 line 584
  52. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4322 line 586
  53. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4323 line 607
  54. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4323 line 609
  55. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4324 line 630
  56. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4324 line 632
  57. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4325 line 653
  58. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4325 line 655
  59. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4337 line 676
  60. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4337 line 678
  61. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4338 line 699
  62. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4338 line 701
  63. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4339 line 722
  64. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4339 line 724
  65. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4341 line 745
  66. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4341 line 747
  67. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4343 line 768
  68. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4343 line 770
  69. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4344 line 791
  70. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4344 line 793
  71. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4346 line 814
  72. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4346 line 816
  73. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4349 line 837
  74. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4349 line 839
  75. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4350 line 860
  76. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4350 line 862
  77. def OAI.MUB6.Certificate.MixedSemantics.singletonSmall4351 line 883
  78. theorem OAI.MUB6.Certificate.MixedSemantics.singleton4351 line 885