mathlib

0d249d70 - feat(analysis/normed_space/*): group of units of a normed ring is open (#3210)

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](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Inversion.20is.20analytic)) 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](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Dangerous.20instance)) * `algebra.group_with_zero`: the `subsingleton_or_nonzero` dichotomy for monoids with zero ([Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/zero.20ring/near/202202187)) (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](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Finite.20geometric.20series))