OAI/Combinatorics/Progressions/Estimates/WeightedDerivationDrop.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.weightedDerivation_mul line 15
2. theorem OAI.Erdos3.weightedDerivation_monomial_one line 25
3. theorem OAI.Erdos3.weightedDerivation_monomial line 58
4. theorem OAI.Erdos3.weightedDerivation_apply line 69
5. theorem OAI.Erdos3.weightedDerivation_apply_le line 85
6. theorem OAI.Erdos3.weightedDerivation_bracket line 93
7. theorem OAI.Erdos3.weightedDerivation_pow line 103
8. theorem OAI.Erdos3.weightedDerivation_pow_eq_zero line 115