Theorems · Theorem · special functions
PeriodPair.hasFPowerSeriesAt_derivWeierstrassPExcept
∀ (L : PeriodPair) (l : ℂ),
HasFPowerSeriesAt (L.derivWeierstrassPExcept l)
(FormalMultilinearSeries.ofScalars ℂ fun i => (↑i + 1) * (↑i + 2) * L.sumInvPow l (i + 3)) l- Cited by
- 1 results in Mathlib
- Foundations
- Depth 305 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- SetLike.coeproof · cited by 8,199
- Complexstatement and proof · cited by 5,565
- Compl.complproof · cited by 2,925
- LT.lt.leproof · cited by 2,189
- sub_selfproof · cited by 996
- sub_zeroproof · cited by 938
- Metric.closedBallproof · cited by 704
- zero_powproof · cited by 361
- Filter.HasBasis.mem_iffproof · cited by 193
- inv_zeroproof · cited by 184
- PeriodPairstatement and proof · cited by 94
Cited by1
Results whose statement or proof uses this declaration.
- PeriodPair.iteratedDeriv_derivWeierstrassPExcept_selfproof · cited by 1