OAI/Combinatorics/Progressions/Estimates/SecondDifferenceVectorEquivalence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.mixedSecondDifferenceInput line 12
2. def OAI.Erdos3.NativeMultidegreeNilcharacter.mixedSecondDifferenceWithShift line 17
3. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedSecondDifferenceWithShift_unit line 27
4. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.exists_mixed_second_difference_translation line 34
5. def OAI.Erdos3.mixedSecondDifferenceHom line 92
6. def OAI.Erdos3.mixedSecondDifferenceVector line 102
7. theorem OAI.Erdos3.NativeMultidegreeNilcharacter.mixedSecondDifferenceWithShift_zero line 107
8. theorem OAI.Erdos3.NativeIntegerVectorEquivalence.exists_second_difference_budget line 115