From cbd763eb0a306a2240a976ce9d82fc38bfdab649 Mon Sep 17 00:00:00 2001
From: MetalCreator666 <57985847+MetalCreator666@users.noreply.github.com>
Date: Fri, 6 Dec 2024 18:22:10 +0100
Subject: [PATCH] Added ederiv properties

---
 DeRhamCohomology/DifferentialForm.lean | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/DeRhamCohomology/DifferentialForm.lean b/DeRhamCohomology/DifferentialForm.lean
index e834271..4f12cfe 100644
--- a/DeRhamCohomology/DifferentialForm.lean
+++ b/DeRhamCohomology/DifferentialForm.lean
@@ -55,6 +55,18 @@ def constOfIsEmpty (x : F) : Ω^0⟮E, F⟯ :=
 def ederiv (ω : Ω^n⟮E, F⟯) : Ω^n + 1⟮E, F⟯ :=
   fun x ↦ .uncurryFin (fderiv ℝ ω x)
 
+theorem ederiv_add (ω₁ ω₂ : Ω^n⟮E, F⟯) {x : E} (hω₁ : DifferentiableAt ℝ ω₁ x)
+    (hω₂ : DifferentiableAt ℝ ω₂ x) : ederiv (ω₁ + ω₂) x = ederiv ω₁ x + ederiv ω₂ x := by
+  simp [ederiv, fderiv_add' hω₁ hω₂, uncurryFin_add]
+
+theorem ederiv_smul (ω : Ω^n⟮E, F⟯) (c : ℝ) {x : E} (hω : DifferentiableAt ℝ ω x):
+    ederiv (c • ω) x = c • ederiv ω x := by
+  simp [ederiv, fderiv_const_smul' hω, uncurryFin_smul]
+
+theorem ederiv_constOfIsEmpty (x : E) (y : F) :
+    ederiv (constOfIsEmpty y) x = .uncurryFin (fderiv ℝ (constOfIsEmpty y) x) :=
+  rfl
+
 theorem Filter.EventuallyEq.ederiv_eq {ω₁ ω₂ : Ω^n⟮E, F⟯} {x : E}
     (h : ω₁ =ᶠ[𝓝 x] ω₂) : ederiv ω₁ x = ederiv ω₂ x := by
   ext v