Theorems · Theorem · functional analysis

spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul

∀ (𝕜 : Type u_1) {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A] (a : A),
  HasFPowerSeriesOnBall (fun z => Ring.inverse (1 - z • a))
    (fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 (↑‖a‖₊)⁻¹

In a Banach algebra A over a nontrivially normed field 𝕜, for any a : A the power series with coefficients a ^ n represents the function (1 - z • a)⁻¹ in a disk of radius ‖a‖₊⁻¹.

Defined in

Mathlib.Analysis.Normed.Algebra.Spectrum

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraHasSummableGeomSeries