OAI/Combinatorics/Progressions/Estimates/MixedFixedReduction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NativeMixedReductionData.translationCodeEquiv line 15
2. instance OAI.Erdos3.NativeMixedReductionData.translationCodeFintype line 25
3. def OAI.Erdos3.NativeMixedReductionData.reductionCodeEquiv line 29
4. instance OAI.Erdos3.NativeMixedReductionData.reductionCodeFintype line 37
5. theorem OAI.Erdos3.NativeMixedReductionData.translationCode_card line 41
6. theorem OAI.Erdos3.NativeMixedReductionData.reductionCode_card line 72
7. theorem OAI.Erdos3.NativeMixedReductionData.double_translation line 104
8. theorem OAI.Erdos3.NativeMixedReductionData.reduce_quadruple line 159
9. theorem OAI.Erdos3.NativeMixedReductionData.reduce_family line 198