properties curryFin + interior product definition (know its a bit mes…

…sy to do this in this branch but well...)

DeRhamCohomology/ContinuousAlternatingMap/Curry.lean

@@ -102,6 +102,21 @@ def curryFin (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : E →L[𝕜] E [⋀^Fin n]
       apply le_of_eq
       exact ContinuousMultilinearMap.curryLeft_norm f.toContinuousMultilinearMap
 
+theorem curryFin_apply (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) (m : Fin n → E) :
+    curryFin f x m = f (Fin.cons x m) :=
+  rfl
+
+theorem curryFin_add (f g : E [⋀^Fin (n + 1)]→L[𝕜] F) :
+    curryFin (f + g) = curryFin f + curryFin g := by
+  ext e v
+  simp [curryFin_apply]
+
+theorem curryFin_smul {M : Type*} [Monoid M] [DistribMulAction M F] [ContinuousConstSMul M F]
+    [SMulCommClass 𝕜 M F] (c : M) (f : E [⋀^Fin (n + 1)]→L[𝕜] F) :
+    curryFin (c • f) = c • curryFin f := by
+  ext e v
+  simp [curryFin_apply]
+
 variable [DecidableEq ι] [DecidableEq ι']
 
 /-- summand used in `ContinuousAlternatingMap.uncurrySum` -/

DeRhamCohomology/DifferentialForm.lean

@@ -210,6 +210,10 @@ theorem pullback_constOfIsEmpty (f : E → F) (g : G) :
     pullback f (constOfIsEmpty g) = fun _ ↦ (ContinuousAlternatingMap.constOfIsEmpty ℝ E (Fin 0) g) :=
   rfl
 
+/- Interior product of differential forms -/
+def iprod (ω : Ω^(m + 1)⟮E, F⟯) (v : E → E) : Ω^m⟮E, F⟯ :=
+    fun e => ContinuousAlternatingMap.curryFin (ω e) (v e)
+
 /- Wedge product of differential forms -/
 def wedge_product (ω₁ : Ω^m⟮E, F⟯) (ω₂ : Ω^n⟮E, F'⟯) (f : F →L[ℝ] F' →L[ℝ] F'') :
     Ω^(m + n)⟮E, F''⟯ := fun e => ContinuousAlternatingMap.wedge_product (ω₁ e) (ω₂ e) f