added Playground2

WegmannDavid · WegmannDavid · commit 98a4848f1c41 · 2026-04-13T19:35:46.000+02:00
diff --git a/FunGrad/Playground2.lean b/FunGrad/Playground2.lean
@@ -69,4 +69,4 @@ def DiffMap.comp {n m k : ℕ} (g : DiffMap m k) (f : DiffMap n m) : DiffMap n k
 
 def DiffMap.id {n} : DiffMap n n where
   f x := x
-  deriv x := sorry -- zero
+  deriv x := sorry
