OAI/Combinatorics/Progressions/Polynomial/PolynomialShearAffineExponential.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialDerivationDrop line 16
  2. theorem OAI.Erdos3.polynomialDerivationDrop_antitone line 29
  3. theorem OAI.Erdos3.polynomialDerivationDrop_bracket line 34
  4. def OAI.Erdos3.polynomialLoweringLieAlgebra line 40
  5. abbrev OAI.Erdos3.PolynomialShearLieAlgebra line 46
  6. def OAI.Erdos3.polynomialShearLayer line 49
  7. theorem OAI.Erdos3.mem_polynomialShearLayer line 53
  8. theorem OAI.Erdos3.polynomialShearLayer_antitone line 57
  9. theorem OAI.Erdos3.polynomialShearLayer_one line 62
  10. theorem OAI.Erdos3.polynomialShearLayer_bracket line 68
  11. theorem OAI.Erdos3.polynomialShearLayer_terminal line 75
  12. def OAI.Erdos3.polynomialShearFiltration line 86
  13. theorem OAI.Erdos3.polynomialShear_lowerCentralSeries_eq_bot line 94
  14. theorem OAI.Erdos3.polynomialShear_group_nilpotencyClass_le line 99
  15. abbrev OAI.Erdos3.PolynomialShearIndex line 115
  16. def OAI.Erdos3.polynomialShearCoordinates line 118
  17. theorem OAI.Erdos3.polynomialShearCoordinates_apply line 143
  18. def OAI.Erdos3.polynomialShearBasis line 146
  19. theorem OAI.Erdos3.polynomialShearBasis_repr line 151
  20. def OAI.Erdos3.polynomialShearMonomial line 155
  21. theorem OAI.Erdos3.polynomialShearMonomial_X line 168
  22. def OAI.Erdos3.polynomialShearBoundedCoordinates line 190
  23. theorem OAI.Erdos3.polynomialShearBoundedCoordinates_injective line 204
  24. theorem OAI.Erdos3.polynomialShear_moduleFinite line 213
  25. theorem OAI.Erdos3.polynomialShear_finrank_le line 220
  26. theorem OAI.Erdos3.polynomialShear_finrank_fin line 233
  27. theorem OAI.Erdos3.polynomialShear_X_mass_of_coordinates line 250
  28. theorem OAI.Erdos3.polynomialShear_pow_degree line 267
  29. theorem OAI.Erdos3.polynomialShear_pow_mass line 274
  30. theorem OAI.Erdos3.polynomialShear_pow_mass_of_coordinates line 293
  31. def OAI.Erdos3.polynomialShearEnd line 317
  32. theorem OAI.Erdos3.polynomialShearEnd_apply_coe line 328
  33. def OAI.Erdos3.polynomialShearAction line 332
  34. theorem OAI.Erdos3.polynomialShearEnd_pow_coe line 355
  35. theorem OAI.Erdos3.polynomialShearEnd_pow_eq_zero line 365
  36. theorem OAI.Erdos3.polynomialShearEnd_isNilpotent line 374
  37. theorem OAI.Erdos3.polynomialShearAction_injective line 377
  38. theorem OAI.Erdos3.polynomialShearMonomial_repr line 398
  39. theorem OAI.Erdos3.polynomialShearBasis_eq_monomial line 415
  40. def OAI.Erdos3.polynomialShearDeficit line 420
  41. theorem OAI.Erdos3.polynomialShearDeficit_pos line 424
  42. theorem OAI.Erdos3.polynomialShearBasis_mem_layer line 430
  43. theorem OAI.Erdos3.polynomialShearLayer_span line 450
  44. def OAI.Erdos3.polynomialShearIndexFintype line 469
  45. theorem OAI.Erdos3.polynomialShearDeficit_le line 479
  46. def OAI.Erdos3.polynomialShearExpOn line 495
  47. theorem OAI.Erdos3.polynomialShearExpOn_sum line 499
  48. theorem OAI.Erdos3.polynomialShearExpOn_mono line 507
  49. def OAI.Erdos3.weightedPolynomialMul line 520
  50. theorem OAI.Erdos3.polynomialShearExpOn_mul line 536
  51. theorem OAI.Erdos3.polynomialShearBasis_coordinate_eval line 564
  52. def OAI.Erdos3.polynomialShearExp line 603
  53. theorem OAI.Erdos3.polynomialShearExp_eq_on line 608
  54. theorem OAI.Erdos3.polynomialShearExp_eq_sum line 614
  55. theorem OAI.Erdos3.polynomialShearExp_degree line 621
  56. theorem OAI.Erdos3.polynomialShearExp_add line 627
  57. theorem OAI.Erdos3.polynomialShearExp_smul line 639
  58. theorem OAI.Erdos3.polynomialShearExp_mul line 648
  59. theorem OAI.Erdos3.polynomialShearExp_C line 659
  60. def OAI.Erdos3.polynomialShearExpHom line 664
  61. theorem OAI.Erdos3.polynomialShearExp_sub_lower line 673
  62. def OAI.Erdos3.polynomialShearExpAut line 689
  63. theorem OAI.Erdos3.polynomialShearExpAut_apply line 694
  64. theorem OAI.Erdos3.polynomialShearExp_eq_add_of_sq_eq_zero line 709
  65. theorem OAI.Erdos3.polynomialShearExp_X_of_derivation_eq_C line 727