Theorems · Theorem · functional analysis

NormedRing.inverse_add_norm_diff_first_order

∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ),
  (fun t => Ring.inverse (↑x + t) - ↑x⁻¹) =O[nhds 0] fun t => ‖t‖

The function fun t ↦ Ring.inverse (x + t) - x⁻¹ is O(t) as t → 0.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries