Theorems · Theorem · complex analysis

Real.one_div_sub_pow_hasFPowerSeriesOnBall_zero

∀ (a : ℕ) {r : ℝ},
  r ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (r - x) ^ (a + 1))
      (FormalMultilinearSeries.ofScalars ℝ fun n => (r ^ (n + a + 1))⁻¹ * ↑((a + n).choose a)) 0 ‖r‖ₑ

Defined in

Mathlib.Analysis.Analytic.Binomial

Cited by

2 results in Mathlib

Foundations

Depth 296 from the axioms · uses propext, Classical.choice, Quot.sound