Theorems · Theorem · real analysis
AnalyticAt.hasFPowerSeriesAt
∀ {𝕜 : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜},
AnalyticAt 𝕜 f x →
HasFPowerSeriesAt f (FormalMultilinearSeries.ofScalars 𝕜 fun n => iteratedDeriv n f x / ↑n.factorial) x- Cited by
- 7 results in Mathlib
- Foundations
- Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites34
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- NormedAddCommGroupproof · cited by 15,752
- NormedSpaceproof · cited by 12,499
- ENNRealproof · cited by 9,879
- NontriviallyNormedFieldstatement and proof · cited by 8,742
- Finset.univproof · cited by 3,473
- one_mulproof · cited by 2,841
- CompleteSpacestatement and proof · cited by 2,532
- Finset.prodproof · cited by 2,356
- mul_commproof · cited by 2,262
- Nat.cast_zeroproof · cited by 1,870
- CharZerostatement and proof · cited by 932
Cited by7
Results whose statement or proof uses this declaration.
- AnalyticOn.hasFPowerSeriesOnSubballproof · cited by 2
- AnalyticAt.analyticAt_localInverseproof · cited by 2
- hasFPowerSeriesAt_clog_oneproof · cited by 2
- PeriodPair.iteratedDeriv_derivWeierstrassPExcept_selfproof · cited by 1
- UpperHalfPlane.hasFPowerSeries_cuspFunctionproof · cited by 1
- PeriodPair.iteratedDeriv_weierstrassPExcept_selfproof · cited by 0
- ProbabilityTheory.hasFPowerSeriesAt_mgfproof · cited by 0