OAI/Combinatorics/Progressions/Estimates/SquarefreeCoefficients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.squarefreeCoefficients line 15
2. theorem OAI.Erdos3.squarefreeCoefficients_apply line 20
3. theorem OAI.Erdos3.squarefreeCoefficients_monomial_self line 23
4. theorem OAI.Erdos3.squarefreeCoefficients_monomial_ne line 28
5. theorem OAI.Erdos3.squarefreeCoefficients_surjective line 34
6. theorem OAI.Erdos3.monomial_mem_squarefreeKernel line 47