Commit 2024-09-10 12:32 e64b85df

View on Github →

feat(Lie/Derivation): general Leibniz rule for Lie derivatives (#16641) This PR adds the general Leibniz rule for Lie derivatives

Estimated changes

Modified Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.prod_Ico_add_right_sub_eq

added theorem Finset.prod_range_eq_mul_Ico

Modified Mathlib/Algebra/Lie/Derivation/Basic.lean

added theorem LieDerivation.iterate_apply_lie'

added theorem LieDerivation.iterate_apply_lie