OAI/Combinatorics/Progressions/Linear/GradeProjectionRemainder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.basisGradeProjection_eq_zero_of_mem_higher line 16
2. theorem OAI.Erdos3.sub_basisGradeProjection_mem_higher line 27
3. theorem OAI.Erdos3.BasisGradedSubmodule.mem_sup_higher_of_grade line 42
4. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeProjection_eq_zero_of_mem_next_layer line 66
5. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeProjection_bch_triple line 74
6. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeProjection_normalized_splitting line 85
7. theorem OAI.Erdos3.NilpotentLieFiltration.realGradeProjection_normalized_residual_mem line 101