OAI/Combinatorics/Progressions/Lattices/MixedTranslationAffineInput.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.mixedTranslationSlope line 9
2. def OAI.Erdos3.mixedTranslationIntercept line 13
3. theorem OAI.Erdos3.mixedTranslationSample_affine line 18
4. theorem OAI.Erdos3.mixedTranslationSlope_replaced_none line 28
5. theorem OAI.Erdos3.mixedTranslationSlope_replaced_vanishes line 32