OAI/Combinatorics/Progressions/Estimates/FastGradedRelativeInvariance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_basis_height line 19
2. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedDifference_mem_second line 30
3. theorem OAI.Erdos3.NilpotentLieFiltration.fastGradedRelativeKernel_graded line 49
4. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastGradedRelative_le_second line 65
5. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastGradedRelative_low_projection line 70
6. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastGradedRelative_graded line 82
7. theorem OAI.Erdos3.NilpotentLieFiltration.fullFastGradedRelative_lie_mem line 113
8. theorem OAI.Erdos3.NilpotentLieFiltration.realFullFastGradedRelative_lie_mem line 134