OAI/Combinatorics/Progressions/Linear/RankHorizontalSymbol.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.DegreeRankLieFiltration.rankLayerCoefficient line 15
2. theorem OAI.Erdos3.DegreeRankLieFiltration.rankLayerCoefficient_coe line 22
3. def OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalCoefficient line 26
4. theorem OAI.Erdos3.DegreeRankLieFiltration.bracket_coefficient_mem_rank_two line 30
5. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalCoefficient_lie line 55
6. def OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalSymbolCoefficient line 74
7. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalSymbolCoefficient_map line 82
8. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalSymbolCoefficient_lie line 87
9. theorem OAI.Erdos3.DegreeRankLieFiltration.higherHorizontalCoefficient_translate line 95