Theorems · Theorem · complex analysis

Real.hasFPowerSeriesOnBall_ofScalars_mul_add_zero

∀ (a b : ℝ),
  HasFPowerSeriesOnBall (fun x => (b - a) / (1 - x) + a / (1 - x) ^ 2)
    (FormalMultilinearSeries.ofScalars ℝ fun x => a * ↑x + b) 0 1

∑ (ai + b) zⁱ = (b - a) / (1 - z) + a / (1 - z)²

Defined in

Mathlib.Analysis.Analytic.Binomial

Cited by

1 results in Mathlib

Foundations

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