Commit 2026-03-12 19:24 294f8be7

View on Github →

feat: covariant derivatives on vector bundles (#36279) From the path towards the the Levi-Civita connection and Riemannian geometry.

Estimated changes

Modified Mathlib.lean

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

added theorem extDerivFun_add

added theorem extDerivFun_zero

Created Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean

added theorem ContMDiffCovariantDerivativeOn.affine_combination

added theorem ContMDiffCovariantDerivativeOn.finite_affine_combination

added theorem CovariantDerivative.ContMDiffCovariantDerivative.affine_combination

added theorem CovariantDerivative.ContMDiffCovariantDerivative.finite_affine_combination

added def CovariantDerivative.addOneForm

added def CovariantDerivative.affine_combination

added theorem CovariantDerivative.contMDiffCovariantDerivativeOn_univ_iff

added def CovariantDerivative.difference

added def CovariantDerivative.finite_affine_combination

added theorem CovariantDerivative.isCovariantDerivativeOn

added def CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover

added theorem CovariantDerivative.of_isCovariantDerivativeOn_of_open_cover_coe

added theorem CovariantDerivative.zero

added structure CovariantDerivative

added theorem IsCovariantDerivativeOn.add_one_form

added theorem IsCovariantDerivativeOn.affine_combination

added theorem IsCovariantDerivativeOn.congr_of_eqOn

added theorem IsCovariantDerivativeOn.congr_of_eventuallyEq

added def IsCovariantDerivativeOn.difference

added theorem IsCovariantDerivativeOn.difference_apply

added theorem IsCovariantDerivativeOn.finite_affine_combination

added theorem IsCovariantDerivativeOn.iUnion

added theorem IsCovariantDerivativeOn.mono

added theorem IsCovariantDerivativeOn.smul_const

added theorem IsCovariantDerivativeOn.zero

added structure IsCovariantDerivativeOn

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem ContinuousLinearMap.smulRight_zero

added theorem ContinuousLinearMap.zero_smulRight