OAI/Combinatorics/Progressions/Polynomial/PolynomialLiftArrays.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos3.VectorPolynomial.assembleFamilyline 15 - theorem
OAI.Erdos3.VectorPolynomial.coefficients_assembleFamilyline 21 - def
OAI.Erdos3.liftQuotientArrayline 34 - theorem
OAI.Erdos3.coefficients_liftQuotientArrayline 39 - theorem
OAI.Erdos3.liftQuotientArray_coefficient_eq_zeroline 45 - theorem
OAI.Erdos3.bracket_system_matches_lift_arrayline 52