English
For a unit x and natural n, near 0, the inverse of x + t has an nth-order expansion: a finite sum of powers of −x⁻¹ t times x⁻¹ plus (−x⁻¹ t)^n times inverse(x + t).
Русский
Для единицы x и натурального n около 0 обратное к x + t имеет n-й порядок: конечная сумма степеней (−x⁻¹ t) по умножению на x⁻¹ плюс (−x⁻¹ t)^n умноженное на inverse(x + t).
LaTeX
$$$\forall x\in R^{\times},\; n\in\mathbb{N},\; \text{near }0:\; \text{inverse}(x+t) = \left(\sum_{i=0}^{n-1} (-x^{-1} t)^{i}\right) x^{-1} + (-x^{-1} t)^{n} \text{inverse}(x+t).$$$
Lean4
/-- 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. -/
theorem inverse_add_nth_order (x : Rˣ) (n : ℕ) :
∀ᶠ t in 𝓝 0, inverse ((x : R) + t) = (∑ i ∈ range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (x + t) :=
by
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) := (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'
rw [neg_mul, sub_neg_eq_add] at ht'
conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
rw [ht]
