# Commit 2020-07-04 08:32 0d249d70

View on Github →feat(analysis/normed_space/*): group of units of a normed ring is open (#3210) In a complete normed ring, the group of units is an open subset of the ring (Zulip) Supporting material:

`topology.metric_space.basic`

,`analysis.normed_space.basic`

,`normed_space.operator_norm`

: some lemmas about limits and infinite sums in metric and normed spaces`analysis.normed_space.basic`

,`normed_space.operator_norm`

: left- and right- multiplication in a normed ring (algebra) is a bounded homomorphism (linear map); the algebra/linear-map versions are not needed for the main result but included for completeness`analysis.normed_space.basic`

: a normed algebra is`nonzero`

(not needed for the main result) (Zulip)`algebra.group_with_zero`

: the`subsingleton_or_nonzero`

dichotomy for monoids with zero (Zulip) (written by @jcommelin )`analysis.specific_limits`

: results on geometric series in a complete`normed_ring`

; relies on`algebra.geom_sum`

: "left" variants of some existing "right" lemmas on finite geometric series; relies on`algebra.opposites`

,`algebra.group_power`

,`algebra.big_operators`

: lemmas about the opposite ring (Zulip)