Commit 2026-03-06 15:35 2e3bc242

View on Github →

feat: product rule for Lie bracket on manifolds (#26743) On the path towards geodesics and the Levi-Civita connection.

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean

added theorem fderivWithin_extChartAt_comp_extChartAt_symm_range

added theorem mfderivWithin_extChartAt_symm_inverse_apply

added theorem mfderivWithin_range_extChartAt_symm

added theorem mfderiv_extChartAt_self

Modified Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

added theorem DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm

added theorem MDifferentiableWithinAt.differentiableWithinAt_comp_extChartAt_symm

Modified Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

added theorem VectorField.mfderiv_extChartAt_inverse_comp_mfderivWithin_extChartAT_symm

modified theorem VectorField.mlieBracketWithin_of_mem_nhdsWithin

added theorem VectorField.mlieBracketWithin_smul_left

added theorem VectorField.mlieBracketWithin_smul_right

added theorem VectorField.mlieBracket_smul_left

added theorem VectorField.mlieBracket_smul_right

added theorem VectorField.mpullback_mfderivWithin_apply_smul

Modified Mathlib/Geometry/Manifold/VectorField/Pullback.lean

added theorem VectorField.mpullbackWithin_const_smul

added theorem VectorField.mpullbackWithin_const_smul_apply

modified theorem VectorField.mpullbackWithin_smul

modified theorem VectorField.mpullbackWithin_smul_apply

added theorem VectorField.mpullback_const_smul

added theorem VectorField.mpullback_const_smul_apply

modified theorem VectorField.mpullback_smul

modified theorem VectorField.mpullback_smul_apply