Theorems · Theorem · functional analysis

Units.isOpenEmbedding_val

∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], Topology.IsOpenEmbedding Units.val

In a normed ring with summable geometric series, the coercion from Rˣ (equipped with the induced topology from the embedding in R × R) to R is an open embedding.

Defined in

Mathlib.Analysis.Normed.Ring.Units

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedRingHasSummableGeomSeries