diff --git a/SciLean/FTrans/FwdDeriv/Basic.lean b/SciLean/FTrans/FwdDeriv/Basic.lean
index 4f1d7fde..cc9f08d6 100644
--- a/SciLean/FTrans/FwdDeriv/Basic.lean
+++ b/SciLean/FTrans/FwdDeriv/Basic.lean
@@ -468,3 +468,30 @@ theorem HDiv.hDiv.arg_a4a5.fwdDeriv_comp
       (ydy.1 / zdz.1, (ydy.2 * zdz.1 - ydy.1 * zdz.2) / zdz.1^2) :=
 by 
   unfold fwdDeriv; ftrans
+
+
+-- HPow.hPow ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[ftrans_rule]
+def HPow.hPow.arg_a4.fwdDeriv_at_comp
+  (n : Nat) (x : X) (f : X → K) (hf : DifferentiableAt K f x) 
+  : fwdDeriv K (fun x => f x ^ n) x
+    =
+    fun dx =>
+      let ydy := fwdDeriv K f x dx
+      (ydy.1 ^ n, n * ydy.2 * (ydy.1 ^ (n-1))) :=
+by 
+  unfold fwdDeriv; ftrans
+
+
+@[ftrans_rule]
+def HPow.hPow.arg_a4.fwdDeriv_comp
+  (n : Nat) (f : X → K) (hf : Differentiable K f) 
+  : fwdDeriv K (fun x => f x ^ n)
+    =
+    fun x dx =>
+      let ydy := fwdDeriv K f x dx
+      (ydy.1 ^ n, n * ydy.2 * (ydy.1 ^ (n-1))) :=
+by 
+  unfold fwdDeriv; ftrans
diff --git a/SciLean/FunctionSpaces/Differentiable/Basic.lean b/SciLean/FunctionSpaces/Differentiable/Basic.lean
index 69e8e8cd..f9ba4592 100644
--- a/SciLean/FunctionSpaces/Differentiable/Basic.lean
+++ b/SciLean/FunctionSpaces/Differentiable/Basic.lean
@@ -299,3 +299,14 @@ def HDiv.hDiv.arg_a4a5.Differentiable_comp
   (hf : Differentiable R f) (hg : Differentiable R g) (hx : ∀ x, g x ≠ 0)
   : Differentiable R (fun x => f x / g x)
   := Differentiable.div hf hg hx
+
+
+
+-- HPow.hPow ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+def HPow.hPow.arg_a4a5.Differentiable_comp
+  (n : Nat) (f : X → R) (hf : Differentiable R f) 
+  : Differentiable R (fun x => f x ^ n)
+  := Differentiable.pow hf n
diff --git a/SciLean/FunctionSpaces/DifferentiableAt/Basic.lean b/SciLean/FunctionSpaces/DifferentiableAt/Basic.lean
index d86991a7..d0d43706 100644
--- a/SciLean/FunctionSpaces/DifferentiableAt/Basic.lean
+++ b/SciLean/FunctionSpaces/DifferentiableAt/Basic.lean
@@ -312,3 +312,12 @@ def HDiv.hDiv.arg_a4a5.DifferentiableAt_comp
   : DifferentiableAt R (fun x => f x / g x) x 
   := DifferentiableAt.div hf hg hx
 
+
+-- HPow.hPow ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+def HPow.hPow.arg_a4a5.DifferentiableAt_comp
+  (n : Nat) (x : X) (f : X → R) (hf : DifferentiableAt R f x) 
+  : DifferentiableAt R (fun x => f x ^ n) x
+  := DifferentiableAt.pow hf n