Theorems · Definition · functional analysis

Units.ofNearby

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

In a normed ring with summable geometric series, an element y 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

4 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries