OAI/Combinatorics/Progressions/Nilpotent/DegreeRankLieBrackets.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.rank_span_lie_mem line 12
2. theorem OAI.Erdos3.NilpotentLieFiltration.rankLayer_lie_mem line 28
3. def OAI.Erdos3.NilpotentLieFiltration.rankIdeal line 47
4. theorem OAI.Erdos3.NilpotentLieFiltration.mem_rankIdeal line 55
5. theorem OAI.Erdos3.NilpotentLieFiltration.rankIdeal_le_layerIdeal line 58