Theorems · Theorem · complex analysis
Complex.one_div_sub_pow_hasFPowerSeriesOnBall_zero
∀ (a : ℕ) {z : ℂ},
z ≠ 0 →
HasFPowerSeriesOnBall (fun x => 1 / (z - x) ^ (a + 1))
(FormalMultilinearSeries.ofScalars ℂ fun n => (z ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖z‖ₑ- Defined in
- Mathlib.Analysis.Analytic.Binomial
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 295 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites47
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
- NontriviallyNormedFieldproof · cited by 8,742
- Complexstatement and proof · cited by 5,565
- Monoidproof · cited by 3,887
- mul_oneproof · cited by 3,885
- Finset.univproof · cited by 3,473
- one_mulproof · cited by 2,841
- mul_assocproof · cited by 1,667
- map_zeroproof · cited by 1,614
Cited by3
Results whose statement or proof uses this declaration.
- Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zeroproof · cited by 2
- Real.one_div_sub_pow_hasFPowerSeriesOnBall_zeroproof · cited by 2
- Complex.one_div_sub_hasFPowerSeriesOnBall_zeroproof · cited by 1