OAI/Combinatorics/Progressions/Geometry/CoordinateCopySum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.coordinateCopySum line 11
2. theorem OAI.Erdos3.coordinateCopySum_apply line 27
3. theorem OAI.Erdos3.coordinateCopySum_sum line 31
4. theorem OAI.Erdos3.coordinateCopySum_abs_le line 40
5. theorem OAI.Erdos3.coordinateCopySum_intCast line 51
6. theorem OAI.Erdos3.coordinateCopySum_map line 57
7. theorem OAI.Erdos3.coordinateCopySum_polynomial_degree line 65