OAI/Combinatorics/Progressions/Estimates/PreparationSliceComposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.ResidueBoxSlice.identity_point line 13
2. def OAI.Erdos3.ResidueBoxSlice.integerPolynomial line 17
3. theorem OAI.Erdos3.ResidueBoxSlice.integerPolynomial_degree line 20
4. theorem OAI.Erdos3.ResidueBoxSlice.integerPolynomial_eval line 29
5. def OAI.Erdos3.ResidueBoxSlice.reindexInteger line 35
6. theorem OAI.Erdos3.ResidueBoxSlice.reindexInteger_degree line 38
7. theorem OAI.Erdos3.ResidueBoxSlice.reindexInteger_eval line 43
8. theorem OAI.Erdos3.RankPreparationFamily.compose_slice_identity line 56