OAI/Combinatorics/Progressions/Estimates/FastCoefficientBlocks.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.basisCoordinateProjection_coarser_block line 13
2. theorem OAI.Erdos3.BasisBlockInvariant.coarser line 24
3. theorem OAI.Erdos3.BasisBlockInvariant.graded line 38
4. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareSnd_kernel_monomial_blocks line 58
5. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientFastSubmodule_monomial_blocks line 65
6. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientFastSubmodule_graded line 76