OAI/Combinatorics/Progressions/Polynomial/RelativeSquarePolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeSubmodule line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.normalizedRelative_coefficient_mem_two line 18
3. def OAI.Erdos3.NilpotentLieFiltration.relativeSquarePolynomial line 25
4. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquarePolynomial_coefficient line 33
5. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquarePolynomial_adapted line 38
6. def OAI.Erdos3.NilpotentLieFiltration.relativeSquareLift line 48
7. def OAI.Erdos3.NilpotentLieFiltration.relativeSquareSymbolMap line 82
8. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquareSymbolMap_eq_zero_iff line 86
9. def OAI.Erdos3.NilpotentLieFiltration.normalizedRelativeFirstJet line 107
10. theorem OAI.Erdos3.NilpotentLieFiltration.relativeSquareSymbolMap_eq_iff line 110