Theorems · Theorem · functional analysis

NormedRing.inverse_add_norm_diff_second_order

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

The function fun t ↦ Ring.inverse (x + t) - x⁻¹ + x⁻¹ * t * x⁻¹ is O(t ^ 2) 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