Theorems · Theorem · real analysis

iteratedDerivWithin_pow

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s → ∀ (m k : ℕ), iteratedDerivWithin k (fun x => x ^ m) s x = ↑(m.descFactorial k) * x ^ (m - k)

Defined in: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
Cited by: 1 results in Mathlib
Foundations: Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NontriviallyNormedField

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites38

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
NontriviallyNormedFieldstatement and proof · cited by 8,742
mul_oneproof · cited by 3,885
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
Nat.cast_oneproof · cited by 2,501
zero_addproof · cited by 2,366
Finset.sum_congrproof · cited by 2,323
MulZeroClass.mul_zeroproof · cited by 2,091
Nat.cast_zeroproof · cited by 1,870
MulZeroClass.zero_mulproof · cited by 1,625
Finset.rangeproof · cited by 1,341

Cited by1

Results whose statement or proof uses this declaration.

iteratedDeriv_powproof · cited by 1