Commit 2025-11-05 01:04 d4edd8f7

View on Github →

feat: derivative along the Lie bracket of vector fields (#30490)

Estimated changes

Modified Mathlib/Analysis/Calculus/VectorField.lean

added theorem VectorField.fderivWithin_apply_lieBracket

added theorem VectorField.fderivWithin_apply_lieBracket_of_isSymmSndFDerivWithinAt

added theorem VectorField.fderiv_apply_lieBracket

added theorem VectorField.fderiv_apply_lieBracket_of_isSymmSndFDerivAt

deleted theorem VectorField.lieBracket_fmul_left

added theorem VectorField.lieBracket_smul_left