Commit 2025-07-04 10:05 aa10f25b

feat(Analysis/Calculus/VectorField): Implement product rule for liebrackets (#26725) This adds lemmas for the product rule (or Leibniz rule) for Lie brackets on vector fields. These new lemmas are called lieBracket_smul_left and similar. To accomodate this, rename the existing lemmas {m}lieBracket{Within}_smul_{left,right} to {m}lieBracket{Within}_const_smul_{left,right}. A future PR will add the analogous lemmas for vector fields on manifolds: this is useful to introduce Lie derivatives or covariant derivatives. This PR continues the work from #24932.