OAI/Combinatorics/Progressions/Estimates/FormalLinearLiftReabsorption.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_bound_of_coordinate_bound line 18
2. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_reabsorption_bound line 32
3. theorem OAI.Erdos3.VectorPolynomial.basisPolynomialLift_reabsorption_grid line 47
4. theorem OAI.Erdos3.NilpotentLieBCHGroup.formal_basis_lift_reabsorption_control line 72