OAI/Combinatorics/Progressions/Polynomial/CommonDependentPolynomialIntersections.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NativeRankRelation.CommonData.dependentPolynomialLayer line 23
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.coefficientFreeSpan_le_dependentWordLayer line 27
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentAffinePolynomial_mem line 33
4. def OAI.Erdos3.NativeRankRelation.CommonData.dependentShiftAlgebra line 41
5. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.dependentPolynomial_top_frequency_zero line 48
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.real_dependentPolynomial_top_frequency_zero line 55
7. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.dependentPolynomial_bracket_frequency_zero line 64
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentPolynomialLayer_inf line 98
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.dependentPolynomialLayer_top_inter line 120
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.dependentPolynomial_top_inter_le_ker line 128
11. theorem OAI.Erdos3.NativeRankRelation.CommonData.CoefficientBases.exists_dependent_polynomial_quotient_frequency line 135