bug fix in HasAjdDiff for (.^.)

lecopivo · Nov 22, 2023 · 81a6162 · 81a6162
1 parent 833b291
commit 81a6162
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/SciLean/Core/FunctionPropositions/HasAdjDiff.lean b/SciLean/Core/FunctionPropositions/HasAdjDiff.lean
@@ -351,7 +351,7 @@ by
 
 @[fprop]
 def HPow.hPow.arg_a0.HasAdjDiff_rule
-  (n : Nat) (x : X) (f : X → K) (hf : HasAdjDiff K f)
+  (n : Nat) (f : X → K) (hf : HasAdjDiff K f)
   : HasAdjDiff K (fun x => f x ^ n) := 
 by 
   have ⟨_,_⟩ := hf