OAI/Combinatorics/Progressions/Polynomial/AdaptedPolynomialSubstitution.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.parameterLinearCoordinate line 16
  2. def OAI.Erdos3.parameterPolynomialPullback line 19
  3. theorem OAI.Erdos3.parameterPolynomialPullback_degree line 23
  4. theorem OAI.Erdos3.parameterPolynomialPullback_eval line 33
  5. def OAI.Erdos3.VectorPolynomial.substitute line 56
  6. theorem OAI.Erdos3.VectorPolynomial.substitute_tmul line 60
  7. theorem OAI.Erdos3.VectorPolynomial.coefficients_substitute_monomial line 63
  8. theorem OAI.Erdos3.VectorPolynomial.coefficients_substitute line 69
  9. theorem OAI.Erdos3.VectorPolynomial.eval_substitute line 76
  10. theorem OAI.Erdos3.VectorPolynomial.map_substitute line 84
  11. theorem OAI.Erdos3.VectorPolynomial.substitute_comp line 91
  12. theorem OAI.Erdos3.VectorPolynomial.substitute_X line 100
  13. def OAI.Erdos3.VectorPolynomial.substituteLie line 106
  14. def OAI.Erdos3.VectorPolynomial.coefficientModePolynomial line 126
  15. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_eval line 134
  16. theorem OAI.Erdos3.VectorPolynomial.coefficientModePolynomial_degree line 147
  17. def OAI.Erdos3.NilpotentLieFiltration.Adapted line 173
  18. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_iff_coefficients line 176
  19. def OAI.Erdos3.NilpotentLieFiltration.adaptedSubmodule line 193
  20. theorem OAI.Erdos3.NilpotentLieFiltration.mem_adaptedSubmodule line 203
  21. theorem OAI.Erdos3.NilpotentLieFiltration.monomial_mem_adaptedSubmodule line 206
  22. theorem OAI.Erdos3.NilpotentLieFiltration.lie_mem_adaptedSubmodule line 216
  23. def OAI.Erdos3.NilpotentLieFiltration.adaptedLieSubalgebra line 234
  24. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_bch line 237
  25. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_neg line 243
  26. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_degreeLE line 248
  27. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_map line 254
  28. theorem OAI.Erdos3.NilpotentLieFiltration.exists_adapted_lift line 263
  29. def OAI.Erdos3.NilpotentLieFiltration.polynomialSubgroup line 285
  30. abbrev OAI.Erdos3.NilpotentLieFiltration.PolynomialOrbit line 290
  31. def OAI.Erdos3.NilpotentLieFiltration.PolynomialOrbit.log line 294
  32. theorem OAI.Erdos3.NilpotentLieFiltration.PolynomialOrbit.adapted line 297
  33. theorem OAI.Erdos3.NilpotentLieFiltration.PolynomialOrbit.degreeLE line 300
  34. def OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitOfLog line 303
  35. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitOfLog_log line 306
  36. def OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval line 312
  37. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval_coord line 317
  38. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval_mul line 321
  39. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval_inv line 326
  40. theorem OAI.Erdos3.NilpotentLieFiltration.exists_polynomialOrbit_lift line 330
  41. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitEval_step_zero line 342
  42. def OAI.Erdos3.NilpotentLieFiltration.restrictLieSubalgebra line 360
  43. def OAI.Erdos3.NilpotentLieFiltration.polynomialLayer line 376
  44. theorem OAI.Erdos3.NilpotentLieFiltration.monomial_mem_polynomialLayer line 386
  45. theorem OAI.Erdos3.NilpotentLieFiltration.lie_mem_polynomialLayer line 395
  46. def OAI.Erdos3.NilpotentLieFiltration.polynomialFiltration line 411
  47. def OAI.Erdos3.NilpotentLieFiltration.adaptedPolynomialFiltration line 428
  48. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_substitute line 442
  49. def OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitSubstitute line 458
  50. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitSubstitute_log line 472
  51. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialOrbitSubstitute_eval line 477