OAI/Combinatorics/Progressions/Estimates/WeightedLoweringGroup.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedSupportLT_mono line 14
  2. theorem OAI.Erdos3.weightedSupportLT_le line 18
  3. theorem OAI.Erdos3.weightedSupportLT_succ_le line 22
  4. theorem OAI.Erdos3.weightedSupportLT_zero_eq line 26
  5. theorem OAI.Erdos3.weightedLowering_preserves_degree line 33
  6. theorem OAI.Erdos3.weightedLowering_mul_bounds line 44
  7. theorem OAI.Erdos3.weightedLowering_monomial_one line 58
  8. theorem OAI.Erdos3.weightedLowering_monomial line 95
  9. theorem OAI.Erdos3.weightedLowering_difference line 107
  10. def OAI.Erdos3.polynomialHomDifference line 129
  11. theorem OAI.Erdos3.polynomialHomDifference_pow_eq_zero line 133
  12. theorem OAI.Erdos3.weightedLowering_eq_zero_of_degree line 146
  13. theorem OAI.Erdos3.weightedLowering_injective line 163
  14. theorem OAI.Erdos3.weightedLowering_preimage_degree line 172
  15. theorem OAI.Erdos3.weightedLowering_bijective line 189
  16. def OAI.Erdos3.weightedLoweringEquiv line 198
  17. theorem OAI.Erdos3.weightedLoweringEquiv_apply line 204
  18. theorem OAI.Erdos3.weightedLoweringEquiv_inverse_degree line 209
  19. def OAI.Erdos3.weightedLoweringSubgroup line 228
  20. abbrev OAI.Erdos3.WeightedLoweringAut line 259
  21. theorem OAI.Erdos3.weightedLoweringEquiv_mem line 262
  22. def OAI.Erdos3.WeightedLoweringAut.ofHom line 267
  23. theorem OAI.Erdos3.WeightedLoweringAut.preserves_degree line 272
  24. theorem OAI.Erdos3.WeightedLoweringAut.difference_lower line 277