Theorems · Theorem · several complex variables

hasFPowerSeriesOnBall_inverse_one_sub

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

Defined in

Mathlib.Analysis.Analytic.Constructions

Cited by

3 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraHasSummableGeomSeries