basic rules for revDerivProj(Update)

lecopivo · Nov 22, 2023 · db9a9f9 · db9a9f9
1 parent 81a6162
commit db9a9f9
Show file tree

Hide file tree

Showing 5 changed files with 579 additions and 79 deletions.
diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
@@ -50,6 +50,13 @@ theorem revCDeriv_fst (f : X → Y) (x : X)
 by
   rfl
 
+@[simp, ftrans_simp]
+theorem revCDeriv_snd_zero (f : X → Y) (x : X)
+  : (revCDeriv K f x).2 0 = 0 := 
+by
+  simp[revCDeriv]
+
+
 @[ftrans]
 theorem semiAdjoint.arg_a3.cderiv_rule
   (f : X → Y) (a0 : W → Y) (ha0 : IsDifferentiable K a0)