OAI/Combinatorics/Progressions/Polynomial/HomogeneousRealSymbolPolynomial.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.NilpotentLieFiltration.realSymbolOfPolynomial_homogeneousChartline 18 - theorem
OAI.Erdos3.NilpotentLieFiltration.realPolynomialSymbolHom_homogeneousChartline 58