OAI/Combinatorics/Progressions/Polynomial/PolynomialCoordinateSlice.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.polynomialCoordinateSliceline 12 - theorem
OAI.Erdos3.polynomialCoordinateSlice_evalline 16 - theorem
OAI.Erdos3.polynomialCoordinateSlice_coeffline 21 - theorem
OAI.Erdos3.polynomialCoordinateSlice_degree_leline 27 - theorem
OAI.Erdos3.polynomialCoordinateSlice_coefficient_degreesline 33 - theorem
OAI.Erdos3.polynomialCoordinateSlice_selected_coefficientline 38 - theorem
OAI.Erdos3.polynomialCoordinateSlice_measurable_evalline 44 - theorem
OAI.Erdos3.polynomialCoordinateSlice_measurable_coeffline 57