OAI/Analysis/MutuallyUnbiased/Moments/SmallPartitions.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.EqualityPatterns.blocks1 line 10
  2. def OAI.MUB6.EqualityPatterns.raw1 line 11
  3. def OAI.MUB6.EqualityPatterns.label1 line 12
  4. def OAI.MUB6.EqualityPatterns.family1 line 15
  5. theorem OAI.MUB6.EqualityPatterns.pattern1_0 line 21
  6. theorem OAI.MUB6.EqualityPatterns.covers1 line 26
  7. def OAI.MUB6.EqualityPatterns.blocks2 line 32
  8. def OAI.MUB6.EqualityPatterns.raw2 line 33
  9. def OAI.MUB6.EqualityPatterns.label2 line 34
  10. def OAI.MUB6.EqualityPatterns.family2 line 37
  11. theorem OAI.MUB6.EqualityPatterns.pattern2_0 line 43
  12. theorem OAI.MUB6.EqualityPatterns.pattern2_1 line 49
  13. theorem OAI.MUB6.EqualityPatterns.covers2 line 55
  14. def OAI.MUB6.EqualityPatterns.blocks3 line 66
  15. def OAI.MUB6.EqualityPatterns.raw3 line 67
  16. def OAI.MUB6.EqualityPatterns.label3 line 68
  17. def OAI.MUB6.EqualityPatterns.family3 line 71
  18. theorem OAI.MUB6.EqualityPatterns.pattern3_0 line 77
  19. theorem OAI.MUB6.EqualityPatterns.pattern3_1 line 85
  20. theorem OAI.MUB6.EqualityPatterns.pattern3_2 line 93
  21. theorem OAI.MUB6.EqualityPatterns.pattern3_3 line 101
  22. theorem OAI.MUB6.EqualityPatterns.pattern3_4 line 109
  23. theorem OAI.MUB6.EqualityPatterns.covers3 line 117
  24. def OAI.MUB6.EqualityPatterns.blocks4 line 143
  25. def OAI.MUB6.EqualityPatterns.raw4 line 144
  26. def OAI.MUB6.EqualityPatterns.label4 line 145
  27. def OAI.MUB6.EqualityPatterns.family4 line 148
  28. theorem OAI.MUB6.EqualityPatterns.pattern4_0 line 154
  29. theorem OAI.MUB6.EqualityPatterns.pattern4_1 line 165
  30. theorem OAI.MUB6.EqualityPatterns.pattern4_2 line 176
  31. theorem OAI.MUB6.EqualityPatterns.pattern4_3 line 187
  32. theorem OAI.MUB6.EqualityPatterns.pattern4_4 line 198
  33. theorem OAI.MUB6.EqualityPatterns.pattern4_5 line 209
  34. theorem OAI.MUB6.EqualityPatterns.pattern4_6 line 220
  35. theorem OAI.MUB6.EqualityPatterns.pattern4_7 line 231
  36. theorem OAI.MUB6.EqualityPatterns.pattern4_8 line 242
  37. theorem OAI.MUB6.EqualityPatterns.pattern4_9 line 253
  38. theorem OAI.MUB6.EqualityPatterns.pattern4_10 line 264
  39. theorem OAI.MUB6.EqualityPatterns.pattern4_11 line 275
  40. theorem OAI.MUB6.EqualityPatterns.pattern4_12 line 286
  41. theorem OAI.MUB6.EqualityPatterns.pattern4_13 line 297
  42. theorem OAI.MUB6.EqualityPatterns.pattern4_14 line 308
  43. theorem OAI.MUB6.EqualityPatterns.covers4 line 319