Theorems · Theorem · functional analysis

NormedRing.inverse_add

∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  ∀ᶠ (t : R) in nhds 0, Ring.inverse (↑x + t) = Ring.inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹

The formula Ring.inverse (x + t) = Ring.inverse (1 + x⁻¹ * t) * x⁻¹ holds for t sufficiently small.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries