Commit 2025-03-17 06:31 62226eb7

View on Github →

chore: split long file Mathlib.Geometry.Manifold.VectorField (#23000)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Geometry/Manifold/VectorField.lean to Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

deleted theorem ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq

deleted theorem MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq

deleted theorem VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm

deleted theorem VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt

deleted theorem VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm

deleted def VectorField.mpullback

deleted def VectorField.mpullbackWithin

deleted theorem VectorField.mpullbackWithin_add

deleted theorem VectorField.mpullbackWithin_add_apply

deleted theorem VectorField.mpullbackWithin_apply

deleted theorem VectorField.mpullbackWithin_comp_of_left

deleted theorem VectorField.mpullbackWithin_comp_of_right

deleted theorem VectorField.mpullbackWithin_eq_pullbackWithin

deleted theorem VectorField.mpullbackWithin_id

deleted theorem VectorField.mpullbackWithin_neg

deleted theorem VectorField.mpullbackWithin_neg_apply

deleted theorem VectorField.mpullbackWithin_smul

deleted theorem VectorField.mpullbackWithin_smul_apply

deleted theorem VectorField.mpullbackWithin_univ

deleted theorem VectorField.mpullback_add

deleted theorem VectorField.mpullback_add_apply

deleted theorem VectorField.mpullback_apply

deleted theorem VectorField.mpullback_eq_pullback

deleted theorem VectorField.mpullback_id

deleted theorem VectorField.mpullback_neg

deleted theorem VectorField.mpullback_neg_apply

deleted theorem VectorField.mpullback_smul

deleted theorem VectorField.mpullback_smul_apply

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

added theorem ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq

added theorem MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq

added theorem VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm

added theorem VectorField.eventuallyEq_mpullback_mpullbackWithin_extChartAt

added theorem VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm

added def VectorField.mpullback

added def VectorField.mpullbackWithin

added theorem VectorField.mpullbackWithin_add

added theorem VectorField.mpullbackWithin_add_apply

added theorem VectorField.mpullbackWithin_apply

added theorem VectorField.mpullbackWithin_comp_of_left

added theorem VectorField.mpullbackWithin_comp_of_right

added theorem VectorField.mpullbackWithin_eq_pullbackWithin

added theorem VectorField.mpullbackWithin_id

added theorem VectorField.mpullbackWithin_neg

added theorem VectorField.mpullbackWithin_neg_apply

added theorem VectorField.mpullbackWithin_smul

added theorem VectorField.mpullbackWithin_smul_apply

added theorem VectorField.mpullbackWithin_univ

added theorem VectorField.mpullback_add

added theorem VectorField.mpullback_add_apply

added theorem VectorField.mpullback_apply

added theorem VectorField.mpullback_eq_pullback

added theorem VectorField.mpullback_id

added theorem VectorField.mpullback_neg

added theorem VectorField.mpullback_neg_apply

added theorem VectorField.mpullback_smul

added theorem VectorField.mpullback_smul_apply