feat: local frames in a vector bundle (#30083)

We construct local frames on a vector from local trivialisations. The former constructs, given a trivialisation `e` of the vector bundle and a basis of the model fibre, `Basis.localFrame` is a local frame on `e.baseSet`
A future PR will use this to define the local extension of a tangent vector to a vector field near a point.

From the path towards geodesics and the Levi-Civita connection.

Co-authored-by: Patrick Massot [patrickmassot@free.fr](mailto:patrickmassot@free.fr)
Co-authored-by: michaellee94 <michael.a.rodrigues.lee@gmail.com>

Author: grunweg

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -321,6 +321,30 @@ end AddEquiv
 
 namespace LinearMap
 
+/-- Pointwise application of a family of linear forms to a family of vectors -/
+def piApply {V : M → Type*} [CommSemiring R] [∀ x, AddCommMonoid (V x)] [∀ x, Module R (V x)] :
+    (Π x : M, V x →ₗ[R] R) →ₗ[R] (Π x : M, V x) →ₗ[R] M → R where
+  toFun e :=
+    { toFun s x := e x (s x)
+      map_add' := by intros; ext; simp
+      map_smul' := by intros; ext; simp }
+  map_add' := by intros; ext; simp
+  map_smul' := by intros; ext; simp
+
+@[simp]
+theorem piApply_apply {V : M → Type*}
+    [CommSemiring R] [∀ x, AddCommMonoid (V x)] [∀ x, Module R (V x)]
+    (e : Π x : M, V x →ₗ[R] R) (s : Π x : M, V x) :
+    piApply e s = fun x ↦ e x (s x) :=
+  rfl
+
+@[simp]
+theorem piApply_apply_apply {V : M → Type*}
+    [CommSemiring R] [∀ x, AddCommMonoid (V x)] [∀ x, Module R (V x)]
+    (e : Π x : M, V x →ₗ[R] R) (s : Π x : M, V x) (x : M) :
+    piApply e s x = e x (s x) :=
+  rfl
+
 variable (R S M)
 variable [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M]