OAI/Combinatorics/Progressions/Polynomial/SquarePolynomialCoordinates.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.squareDiagonalLie line 14
  2. def OAI.Erdos3.NilpotentLieFiltration.squareFstPolynomialMap line 20
  3. def OAI.Erdos3.NilpotentLieFiltration.squareSndPolynomialMap line 24
  4. def OAI.Erdos3.NilpotentLieFiltration.squareDiagonalPolynomialMap line 28
  5. theorem OAI.Erdos3.NilpotentLieFiltration.squareFstPolynomialMap_coefficient line 33
  6. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndPolynomialMap_coefficient line 40
  7. theorem OAI.Erdos3.NilpotentLieFiltration.squareDiagonalPolynomialMap_coefficient line 47
  8. theorem OAI.Erdos3.NilpotentLieFiltration.square_polynomial_ext line 54
  9. theorem OAI.Erdos3.NilpotentLieFiltration.squareFstPolynomialMap_diagonal line 68
  10. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndPolynomialMap_diagonal line 76
  11. theorem OAI.Erdos3.NilpotentLieFiltration.squareFstPolynomialMap_relative line 84
  12. theorem OAI.Erdos3.NilpotentLieFiltration.squareSndPolynomialMap_relative line 95
  13. def OAI.Erdos3.NilpotentLieFiltration.squareDiagonalSymbolMap line 106
  14. theorem OAI.Erdos3.NilpotentLieFiltration.squareDiagonalSymbolMap_symbol line 111