Theorems · Theorem · functional analysis

NormedRing.inverse_add_nth_order

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

The formula Ring.inverse (x + t) = (∑ i ∈ Finset.range n, (- x⁻¹ * t) ^ i) * x⁻¹ + (- x⁻¹ * t) ^ n * Ring.inverse (x + t) holds for t sufficiently small.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries