Theorems · Theorem · real analysis

contDiffAt_ringInverse

∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {R : Type u_3} [inst_1 : NormedRing R]
  [inst_2 : NormedAlgebra 𝕜 R] [HasSummableGeomSeries R] (x : Rˣ), ContDiffAt 𝕜 n Ring.inverse ↑x

In a complete normed algebra, the operation of inversion is C^n, for all n, at each invertible element, as it is analytic.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Operations

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingNormedAlgebraHasSummableGeomSeries