OAI/Combinatorics/Progressions/Linear/FullFastRelativeSpanning.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.reducedSquareGradedSndMap_basis_height line 24
2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_fast_graded_relative_kernel_generators line 32
3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_bounded_full_fast_relative_generators line 59
4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_fast_relative_generators_exp line 79