OAI/Combinatorics/Progressions/Polynomial/FirstCoefficientPolynomialDerivative.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedPolynomial line 15
  2. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedPolynomial_apply line 19
  3. def OAI.Erdos3.NilpotentLieFiltration.adaptedGradedPolynomialLie line 23
  4. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedGradedPolynomialLie_apply line 27
  5. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedPolynomial_lie line 31
  6. def OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial line 47
  7. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_map line 60
  8. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_coordinate line 67
  9. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_injective line 81
  10. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_homogeneous line 89
  11. theorem OAI.Erdos3.NilpotentLieFiltration.firstCoefficientGradedPolynomial_horizontal line 100
  12. def OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial line 123
  13. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_realEquiv line 129
  14. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_tmul line 135
  15. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_coordinate line 143
  16. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_coordinate_of_ne line 157
  17. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_injective line 168
  18. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_homogeneous line 176
  19. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_bound line 187
  20. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_grid line 199
  21. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_horizontal line 217
  22. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedShiftedGradedPolynomial line 246
  23. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie line 252
  24. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedShiftedGradedPolynomial_tensor line 258
  25. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_tensor line 263
  26. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_apply line 267
  27. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialLie_symbol line 281
  28. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedShiftedGradedPolynomial_lie line 296
  29. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_map line 310
  30. def OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomialHom line 330
  31. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedShiftedGradedPolynomial_adjoint line 335
  32. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_adjoint line 351
  33. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftedGradedPolynomial_directionalDerivative line 381
  34. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedShiftedGradedPolynomial_directionalDerivative line 390
  35. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomial_firstJet line 414
  36. theorem OAI.Erdos3.NilpotentLieFiltration.realAdaptedGradedPolynomial_logDerivative line 429
  37. theorem OAI.Erdos3.NilpotentLieFiltration.realFirstCoefficientGradedPolynomial_direction line 450