English
In a normed ring with summable geometric series, the element 1 - t is a unit with inverse ∑ t^n.
Русский
В нормированном кольце с суммируемой геометрической серией элемент 1 - t является единицей, оборот равен ∑ t^n.
LaTeX
$$$(1 - t) \\\\text{ is a unit and } (1 - t)^{-1} = \\\\sum_{n=0}^{\\\\infty} t^n \\\\text{ when } \\\\|t\\\\| < 1$$$
Lean4
/-- In a normed ring with summable geometric series, a perturbation of `1` by an element `t`
of distance less than `1` from `1` is a unit. Here we construct its `Units` structure. -/
@[simps val]
def oneSub (t : R) (h : ‖t‖ < 1) : Rˣ where
val := 1 - t
inv := ∑' n : ℕ, t ^ n
val_inv := mul_neg_geom_series t h
inv_val := geom_series_mul_neg t h
