Theorems · Theorem · real analysis

hasFDerivAt_ringInverse

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedRing R] [HasSummableGeomSeries R]
  [inst_3 : NormedAlgebra 𝕜 R] (x : Rˣ),
  HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x

At an invertible element x of a normed algebra R, the Fréchet derivative of the inversion operation is the linear map fun t ↦ - x⁻¹ * t * x⁻¹. TODO (low prio): prove a version without assumption [HasSummableGeomSeries R] but within the set of units.

Defined in

Mathlib.Analysis.Calculus.FDeriv.Mul

Cited by

5 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedRingHasSummableGeomSeriesNormedAlgebra