Commit 2025-03-06 18:43 a8ea4840

View on Github →

feat: invariance under diffeomorphisms of the Lie bracket of vector fields on manifolds, and Jacobi identity (#22446)

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

added theorem contMDiffAt_iff_le_ne_infty

added theorem contMDiffAt_iff_nat

added theorem contMDiffWithinAt_iff_le_ne_infty

Modified Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

modified theorem contMDiff_snd_tangentBundle_modelSpace

modified theorem contMDiff_tangentBundleModelSpaceHomeomorph

modified theorem contMDiff_tangentBundleModelSpaceHomeomorph_symm

Modified Mathlib/Geometry/Manifold/VectorField.lean

added theorem ContDiff.mlieBracket_vectorField

added theorem ContMDiffAt.mlieBracket_vectorField

added theorem ContMDiffOn.mlieBracketWithin_vectorField

added theorem VectorField.leibniz_identity_mlieBracket

added theorem VectorField.leibniz_identity_mlieBracketWithin_apply

added theorem VectorField.leibniz_identity_mlieBracket_apply

added theorem VectorField.mpullbackWithin_mlieBracketWithin'

added theorem VectorField.mpullbackWithin_mlieBracketWithin

added theorem VectorField.mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt

added theorem VectorField.mpullback_mlieBracket

added theorem VectorField.mpullback_mlieBracketWithin