OAI/Combinatorics/Progressions/Geometry/TopSupportSubstitution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.mem_weightedSupportLE_one_iff line 13
2. theorem OAI.Erdos3.weightedSupportLT_aeval line 18
3. theorem OAI.Erdos3.polynomialTranslate_sub_mem_weightedSupportLT line 29
4. theorem OAI.Erdos3.fullShiftExponent_weight line 45
5. theorem OAI.Erdos3.full_coefficient_zero_of_lower_support line 50