OAI/Combinatorics/Progressions/Estimates/SquarefreeSplitCount.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.SquarefreeIndex.ofFinset line 16
  2. theorem OAI.Erdos3.SquarefreeIndex.ofFinset_apply line 23
  3. theorem OAI.Erdos3.SquarefreeIndex.support_ofFinset line 28
  4. theorem OAI.Erdos3.SquarefreeIndex.ofFinset_support line 34
  5. theorem OAI.Erdos3.SquarefreeIndex.ofFinset_add_complement line 45
  6. theorem OAI.Erdos3.SquarefreeIndex.blockDegree_ofFinset line 54
  7. theorem OAI.Erdos3.SquarefreeIndex.blockDegree_support line 69
  8. def OAI.Erdos3.fullShiftExponent line 84
  9. theorem OAI.Erdos3.fullShiftExponent_apply line 87
  10. theorem OAI.Erdos3.fullShiftExponent_sum line 90
  11. theorem OAI.Erdos3.exponent_eq_full_or_missing line 95
  12. theorem OAI.Erdos3.SquarefreeIndex.support_subset_of_add line 125
  13. abbrev OAI.Erdos3.SquarefreeSplit line 134
  14. theorem OAI.Erdos3.squarefreeSplit_ext line 138
  15. def OAI.Erdos3.SquarefreeIndex.permute line 159
  16. theorem OAI.Erdos3.SquarefreeIndex.permute_apply line 165
  17. theorem OAI.Erdos3.SquarefreeIndex.permute_symm line 168
  18. theorem OAI.Erdos3.SquarefreeIndex.permute_disjoint line 170
  19. theorem OAI.Erdos3.SquarefreeIndex.permute_disjointAdd line 174
  20. theorem OAI.Erdos3.SquarefreeIndex.permute_zero_iff line 182
  21. theorem OAI.Erdos3.SquarefreeIndex.permute_total line 193
  22. theorem OAI.Erdos3.SquarefreeIndex.permute_blockDegree line 198
  23. def OAI.Erdos3.blockExponent line 223
  24. theorem OAI.Erdos3.blockExponent_apply line 226
  25. theorem OAI.Erdos3.blockExponent_zero line 229
  26. theorem OAI.Erdos3.blockExponent_permute line 233
  27. def OAI.Erdos3.multidegreeFactorial line 239
  28. theorem OAI.Erdos3.multidegreeFactorial_pos line 241
  29. theorem OAI.Erdos3.SquarefreeIndex.permute_weight line 252
  30. def OAI.Erdos3.blockSplitMultiplicity line 272
  31. theorem OAI.Erdos3.multidegreeFactorial_split line 274
  32. def OAI.Erdos3.squarefreeSplitSubsetEquiv line 299
  33. theorem OAI.Erdos3.card_squarefreeSplit line 324
  34. theorem OAI.Erdos3.squarefreeSplit_degree line 335