Theorems · Definition · functional analysis

Units.add

{R : Type u_1} → [inst : NormedRing R] → [HasSummableGeomSeries R] → (x : Rˣ) → (t : R) → ‖t‖ < ‖↑x⁻¹‖⁻¹ → Rˣ

In a normed ring with summable geometric series, a perturbation of a unit x by an element t of distance less than ‖x⁻¹‖⁻¹ from x is a unit. Here we construct its Units structure.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

5 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries