OAI/Combinatorics/Progressions/Polynomial/PolynomialShiftStructure.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.shiftPolynomialLayer line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.shiftPolynomialLayer_antitone line 28
  3. theorem OAI.Erdos3.NilpotentLieFiltration.adapted_mem_shiftPolynomialLayer_one line 32
  4. theorem OAI.Erdos3.NilpotentLieFiltration.monomial_mem_shiftPolynomialLayer line 41
  5. theorem OAI.Erdos3.NilpotentLieFiltration.shiftPolynomialLayer_lie line 51
  6. theorem OAI.Erdos3.NilpotentLieFiltration.directionalDerivative_mem_shiftPolynomialLayer line 67
  7. theorem OAI.Erdos3.NilpotentLieFiltration.shiftPolynomialLayer_terminal line 80
  8. theorem OAI.Erdos3.VectorPolynomial.pderiv_commute line 101
  9. theorem OAI.Erdos3.VectorPolynomial.directionalDerivative_commute line 120
  10. def OAI.Erdos3.VectorPolynomial.directionalLieDerivation line 133
  11. theorem OAI.Erdos3.VectorPolynomial.directionalLieDerivation_apply line 140
  12. def OAI.Erdos3.VectorPolynomial.directionalDerivationLinear line 144
  13. theorem OAI.Erdos3.VectorPolynomial.directionalDerivationLinear_apply line 156
  14. theorem OAI.Erdos3.VectorPolynomial.directionalLieDerivation_lie_eq_zero line 160
  15. def OAI.Erdos3.NilpotentLieFiltration.adaptedShiftDerivation line 180
  16. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftDerivation_coe line 188
  17. def OAI.Erdos3.NilpotentLieFiltration.adaptedShiftDerivationLinear line 193
  18. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftDerivation_commute line 208
  19. def OAI.Erdos3.NilpotentLieFiltration.adaptedShiftAction line 216
  20. theorem OAI.Erdos3.NilpotentLieFiltration.adaptedShiftAction_coe line 230
  21. abbrev OAI.Erdos3.NilpotentLieFiltration.PolynomialShiftAlgebra line 237
  22. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShift_bracket line 242
  23. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShift_direction_bracket line 247
  24. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShift_finiteDimensional line 270
  25. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShift_finrank_le line 283
  26. def OAI.Erdos3.NilpotentLieFiltration.polynomialShiftLayer line 312
  27. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftLayer_antitone line 321
  28. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftLayer_one line 326
  29. theorem OAI.Erdos3.NilpotentLieFiltration.shift_directionalDerivative_mem line 332
  30. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftLayer_lie line 346
  31. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftLayer_terminal line 358
  32. def OAI.Erdos3.NilpotentLieFiltration.polynomialShiftFiltration line 372
  33. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShift_lowerCentralSeries_eq_bot line 380
  34. abbrev OAI.Erdos3.NilpotentLieFiltration.PolynomialShiftGroup line 385
  35. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftGroup_nilpotencyClass_le line 387
  36. def OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis line 405
  37. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_repr_inl line 410
  38. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_repr_inr line 417
  39. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_inl_left line 422
  40. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_inl_right line 430
  41. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_inr_left line 437
  42. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_inr_right line 443
  43. theorem OAI.Erdos3.VectorPolynomial.coefficients_torusDerivative line 464
  44. theorem OAI.Erdos3.VectorPolynomial.torusDerivative_monomial_height line 476
  45. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_inl line 508
  46. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_inr line 516
  47. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_mixed_height line 523
  48. theorem OAI.Erdos3.NilpotentLieFiltration.polynomialShiftBasis_structure_height line 541