Theorems · Theorem · functional analysis

NormedRing.inverse_add_norm_diff_nth_order

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

The function fun t ↦ Ring.inverse (x + t) - (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹ is O(t ^ n) as t → 0.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries