1+M consists of units when M is closed, multiplicative and of norm <1

Let $L$ be a complete normed field and let $M$ be an additive subgroup of $L$ satisfying three conditions: the underlying set of $M$ is closed in $L$; $M$ is closed under multiplication, i.e. $xy \in M$ whenever $x, y \in M$; and every element of $M$ has norm strictly less than $1$. Then for every $x \in M$ there exists $y \in M$ with $(1+x)(1+y) = 1$. Thus each element of the coset $1 + M$ is invertible in $L$ with inverse again lying in $1 + M$; in particular $1 + M$ is a subgroup of $L^{\times}$, although the Lean statement records only the existence of the inverse inside $1 + M$ for a given $x$.

This is the standard statement that a closed, multiplicatively closed additive subgroup of a complete normed field consisting of elements of norm $< 1$ gives rise to the multiplicative group $1 + M$ (the typical case being a maximal ideal of the ring of integers of a local field). It is used in the construction of subgroups of units on which prescribed maps are multiplicative cocycles, at ExtCitation.LocalLevel.exists_subgroup_units_forall_isMulCocycle.