Theorems · Theorem · several complex variables

hasFPowerSeriesOnBall_inverse_one_add

∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A] [Nontrivial A],
  HasFPowerSeriesOnBall (fun x => Ring.inverse (1 + x)) (alternatingGeometricSeries 𝕜 A) 0 1

Defined in

Mathlib.Analysis.Analytic.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraHasSummableGeomSeriesNontrivial