OAI/Combinatorics/Progressions/Estimates/PreparationReindex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.ResidueBoxSlice.reindexIdentity line 13
2. def OAI.Erdos3.ResidueBoxSlice.reindexComp line 18
3. theorem OAI.Erdos3.ResidueBoxSlice.reindexComp_point line 26
4. def OAI.Erdos3.ResidueBoxSlice.reindexPolynomial line 32
5. theorem OAI.Erdos3.ResidueBoxSlice.reindexPolynomial_degree line 35
6. theorem OAI.Erdos3.ResidueBoxSlice.reindexPolynomial_eval line 43
7. theorem OAI.Erdos3.VectorPolynomial.coefficients_reindex_substitute_mem line 53
8. theorem OAI.Erdos3.VectorPolynomial.eval_reindex_slice_substitute line 61