OAI/Combinatorics/Progressions/Estimates/ShiftedAdaptedIdeal.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.shiftedAdaptedSubmodule line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.monomial_mem_shiftedAdaptedSubmodule line 25
3. theorem OAI.Erdos3.NilpotentLieFiltration.lie_mem_shiftedAdaptedSubmodule line 35
4. def OAI.Erdos3.NilpotentLieFiltration.shiftedAdaptedIdeal line 51
5. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_constant line 60
6. def OAI.Erdos3.NilpotentLieFiltration.adaptedConstant line 68
7. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedConstant_mem_shiftedIdeal line 71