English
If hxs ensures unique differentiability within s at x, then derivWithin (fun x => x^m) s x = m x^{m-1}.
Русский
Если условия уникальной дифференцируемости внутри s в точке x выполнены, то derivWithin (t^m) s x = m x^{m-1}.
LaTeX
$$$\\text{derivWithin } (\\lambda t, t^m) \\, s \\, x = m \\cdot x^{m-1}$$$
Lean4
@[simp]
theorem iter_deriv_zpow' (m : ℤ) (k : ℕ) :
(deriv^[k] fun x : 𝕜 => x ^ m) = fun x => (∏ i ∈ Finset.range k, ((m : 𝕜) - i)) * x ^ (m - k) := by
induction k with
| zero => simp only [one_mul, Int.ofNat_zero, id, sub_zero, Finset.prod_range_zero, Function.iterate_zero]
| succ k ihk =>
simp only [Function.iterate_succ_apply', ihk, deriv_const_mul_field', deriv_zpow', Finset.prod_range_succ,
Int.natCast_succ, ← sub_sub, Int.cast_sub, Int.cast_natCast, mul_assoc]
