From 789c1100bcac5c01954ec6445c4eaab8ec85320a Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 12 Jul 2024 09:41:05 +0200
Subject: [PATCH] Update diffOp.lean

---
 Nevanlinna/diffOp.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Nevanlinna/diffOp.lean b/Nevanlinna/diffOp.lean
index 5260e55..1d25981 100644
--- a/Nevanlinna/diffOp.lean
+++ b/Nevanlinna/diffOp.lean
@@ -5,7 +5,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
 
 Let E, F, G be vector spaces over nontrivally normed field 𝕜, a homogeneus
 linear differential operator of order n is a map that attaches to every point e
-of E a linear evaluation 
+of E a linear evaluation
 
 {Continuous 𝕜-multilinear maps E → F in n variables} → G
 
@@ -22,7 +22,7 @@ fun e ↦ D e (iteratedFDeriv 𝕜 n f e)
 -/
 
 @[ext]
-class HomLinDiffOp 
+class HomLinDiffOp
   (𝕜 : Type*) [NontriviallyNormedField 𝕜]
   (n : ℕ)
   (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E]
@@ -59,13 +59,13 @@ noncomputable def Laplace
 
     exact {
       toFun := fun f' ↦ ∑ i, f' ![v i, v i]
-      map_add' := by 
+      map_add' := by
         intro f₁ f₂
-        exact Finset.sum_add_distrib 
+        exact Finset.sum_add_distrib
       map_smul' := by
         intro m f
         exact Eq.symm (Finset.mul_sum Finset.univ (fun i ↦ f ![v i, v i]) m)
-      cont := by 
+      cont := by
         simp
         apply continuous_finset_sum
         intro i _
@@ -86,13 +86,13 @@ noncomputable def Gradient
 
     exact {
       toFun := fun f' ↦ ∑ i, (f' ![v i]) • (v i)
-      map_add' := by 
+      map_add' := by
         intro f₁ f₂
         simp; simp_rw [add_smul, Finset.sum_add_distrib]
       map_smul' := by
         intro m f
         simp; simp_rw [Finset.smul_sum, ←smul_assoc,smul_eq_mul]
-      cont := by 
+      cont := by
         simp
         apply continuous_finset_sum
         intro i _