chore: rename extDerivFun to mvfderiv (#39485)

and generalise to functions taking value in any normed space. (This could be generalised to functions into additive torsors over abelian Lie groups: as we don't have this definition yet and don't need it in our applications, we leave this for the future.)

The new name better reflects that this object is vector-valued. Future PRs will add further API lemmas (such as, about subtraction and negation), custom elaborators and delaborators and a version within a set.

Part of #36036, i.e. from the path towards the Levi-Civita connection and Riemanian curvature.
Related to fixing defeq abuses related to tangent space and scalar multiplication in mathlib.

Co-authored-by: Heather Macbeth [25316162+hrmacbeth@users.noreply.github.com](mailto:25316162+hrmacbeth@users.noreply.github.com)
Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)

Author: grunweg

Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

@@ -18,7 +18,7 @@ differentiability.
 
 In addition to the above, this file provides
 * results about the differentiability of scalar multiplication (`mfderiv_smul` and friends), and
-* `extDerivFun`: the exterior derivative of a scalar function, as a section of the cotangent bundle
+* `mvfderiv`: the exterior derivative of a scalar function, as a section of the cotangent bundle
 
 -/
 
@@ -84,7 +84,7 @@ theorem Differentiable.comp_mdifferentiable {g : F → F'} {f : M → F}
 
 end Module
 
-section ExtChartAt
+section extChartAt
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : M → F}
 
@@ -102,7 +102,7 @@ theorem DifferentiableWithinAt.mdifferentiableWithinAt_of_comp_extChartAt_symm [
   refine (mdifferentiableWithinAt_iff_source_of_mem_source (mem_chart_source H x)).2 ?_
   simpa [extChartAt_self_eq] using hf.mdifferentiableWithinAt
 
-end ExtChartAt
+end extChartAt
 
 /-! ### Linear maps between normed spaces are differentiable -/
 
@@ -396,23 +396,34 @@ lemma fromTangentSpace_mfderiv_smul_apply' (hf : MDiffAt f x) (hg : MDiffAt g x)
 
 end smul
 
-/-! ### Exterior derivative of a scalar function -/
+/-! ### Exterior derivative of a vector-valued function -/
 
-/-- The exterior derivative of a scalar function on `M`, as a section of the cotangent bundle. -/
-noncomputable abbrev extDerivFun (g : M → 𝕜) :
-    Π x : M, TangentSpace I x →L[𝕜] 𝕜 :=
+variable (I) in
+/-- The exterior derivative of a vector-valued function on `M`,
+as a section of the cotangent bundle.
+
+Future: this could be generalised to functions into additive torsors over abelian Lie groups.
+-/
+noncomputable abbrev mvfderiv (g : M → F) :
+    Π x : M, TangentSpace I x →L[𝕜] F :=
   fun x ↦ (NormedSpace.fromTangentSpace <| g x).toContinuousLinearMap ∘L (mfderiv% g x)
 
+@[deprecated (since := "2026-05-17")] alias extDerivFun := mvfderiv
+
 @[simp]
-lemma extDerivFun_add {g g' : M → 𝕜} {x : M} (hg : MDiffAt g x) (hg' : MDiffAt g' x) :
-    extDerivFun (g + g') x = extDerivFun (I := I) g x + extDerivFun g' x := by
-  simp [extDerivFun, mfderiv_add hg hg']
+lemma mvfderiv_add {g g' : M → F} {x : M} (hg : MDiffAt g x) (hg' : MDiffAt g' x) :
+    mvfderiv I (g + g') x = mvfderiv I g x + mvfderiv I g' x := by
+  simp [mvfderiv, mfderiv_add hg hg']
   congr
 
+@[deprecated (since := "2026-05-17")] alias extDerivFun_add := mvfderiv_add
+
 @[simp]
-lemma extDerivFun_zero {x : M} : extDerivFun (I := I) (0 : M → 𝕜) x = 0 := by
-  have : extDerivFun (0 : M → 𝕜) x + extDerivFun (0 : M → 𝕜) x =
-      extDerivFun (I := I) (0 : M → 𝕜) x := by
-    rw [← extDerivFun_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
+lemma mvfderiv_zero {x : M} : mvfderiv (I := I) (0 : M → F) x = 0 := by
+  have : mvfderiv I (0 : M → F) x + mvfderiv I (0 : M → F) x =
+      mvfderiv I (0 : M → F) x := by
+    rw [← mvfderiv_add (by exact mdifferentiable_const ..) (by exact mdifferentiable_const ..)]
     simp
   simpa using this
+
+@[deprecated (since := "2026-05-17")] alias extDerivFun_zero := mvfderiv_zero

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

@@ -96,7 +96,7 @@ structure IsCovariantDerivativeOn
     cov (σ + σ') x = cov σ x + cov σ' x
   leibniz {σ : Π x : M, V x} {g : M → 𝕜} {x}
     (hσ : MDiffAt (T% σ) x) (hg : MDiffAt g x) (hx : x ∈ s := by trivial) :
-    cov (g • σ) x = g x • cov σ x + (extDerivFun g x).smulRight (σ x)
+    cov (g • σ) x = g x • cov σ x + (mvfderiv I g x).smulRight (σ x)
 
 /--
 A covariant derivative ∇ is called of class `C^k` iff, whenever `X` is a `C^k` section and `σ` a
@@ -176,10 +176,10 @@ lemma congr_of_eqOn
   -- Then, it's a chain of (dependent) equalities.
   calc cov σ x
     _ = cov ((ψ : M → 𝕜) • σ) x := by
-      simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, extDerivFun, hψ'.mfderiv]
+      simp [hcov.leibniz hσ hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
     _ = cov ((ψ : M → 𝕜) • σ') x := by rw [funext H]
     _ = cov σ' x := by
-      simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, extDerivFun, hψ'.mfderiv]
+      simp [hcov.leibniz hσ' hψ'.mdifferentiableAt, hψx, mvfderiv, hψ'.mfderiv]
 
 open Filter Set in
 /-- Given a covariant derivative `cov` on a neighborhood `s` of a point `x`, if sections `σ` and
@@ -211,7 +211,7 @@ theorem smul_const (hcov : IsCovariantDerivativeOn F cov s)
     {σ : Π x : M, V x} {x} (a : 𝕜)
     (hσ : MDiffAt (T% σ) x) (hx : x ∈ s := by trivial) :
     cov (a • σ) x = a • cov σ x := by
-  simpa [extDerivFun] using hcov.leibniz (g := fun _ ↦ a) hσ mdifferentiableAt_const
+  simpa [mvfderiv] using hcov.leibniz (g := fun _ ↦ a) hσ mdifferentiableAt_const
 
 end computational_properties
 
@@ -270,15 +270,15 @@ lemma finite_affine_combination {ι : Type*} {s : Finset ι}
     rw [← smul_add, (h i).add hσ hσ' hx]
   leibniz {σ g x} hσ hg hx := by
     calc ∑ i ∈ s, f i x • cov i (g • σ) x
-      _ = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (extDerivFun g x).smulRight (σ x)) := by
+      _ = ∑ i ∈ s, (g x • f i x • cov i σ x + f i x • (mvfderiv I g x).smulRight (σ x)) := by
           congr! 1 with i hi
           rw [(h i).leibniz hσ hg]
-          simp [extDerivFun]
+          simp [mvfderiv]
           module
       _ = g x • ∑ i ∈ s, f i x • cov i σ x +
-        (∑ i ∈ s, f i) x • (extDerivFun g x).smulRight (σ x) := by
+        (∑ i ∈ s, f i) x • (mvfderiv I g x).smulRight (σ x) := by
           rw [Finset.sum_add_distrib, Finset.smul_sum, Finset.sum_apply, Finset.sum_smul]
-      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (extDerivFun g x).smulRight (σ x) := by rw [hf]; simp
+      _ = g x • ∑ i ∈ s, f i x • cov i σ x + (mvfderiv I g x).smulRight (σ x) := by rw [hf]; simp
 
 /-- An affine combination of finitely many `C^k` connections on `u` is a `C^k` connection on `u`. -/
 lemma _root_.ContMDiffCovariantDerivativeOn.finite_affine_combination [IsManifold I 1 M]