OAI/Combinatorics/Progressions/Polynomial/DilationPairPolynomial.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.dilationPair line 13
2. theorem OAI.Erdos3.VectorPolynomial.coefficients_dilationPair line 16
3. theorem OAI.Erdos3.VectorPolynomial.eval_dilationPair line 22
4. theorem OAI.Erdos3.NilpotentLieFiltration.dilationPair_coefficients line 35
5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_dilationPair_orbit line 42
6. theorem OAI.Erdos3.NilpotentLieFiltration.exists_integer_dilationPair_orbit line 53