OAI/Combinatorics/Progressions/Linear/RealCoefficientKernel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFourSpace_eq_sup line 20
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.spaces_le_coefficientFourSpace line 52
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.fourKernel_le_coefficientFourSpace line 57
4. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFourSpace_add_kernel_iff line 63
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.real_fourKernel_le_coefficientFourSpace line 92
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.realCoefficientFourSpace_add_kernel_iff line 107
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.realCoefficientFourSpace_congr_mod_kernel line 113
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.realCoefficientFourSpace_log_product_correction_iff line 124