# Constructing nonarchimedean (ultrametric) normed groups from nonarchimedean normed homs #

This file defines constructions that upgrade `Add(Comm)Group`

to `(Semi)NormedAdd(Comm)Group`

using an `AddGroup(Semi)normClass`

when the codomain is the reals and the hom is nonarchimedean.

## Implementation details #

The lemmas need to assume `[Dist α]`

to be able to be stated, so they take an extra argument
that shows that this distance instance is propositionally equal to the one that comes from the
hom-based `AddGroupSeminormClass.toSeminormedAddGroup f`

construction. To help at use site,
the argument is an autoparam that resolves by definitional equality when using these constructions.

theorem
AddGroupSeminormClass.isUltrametricDist
{F : Type u_1}
{α : Type u_2}
[FunLike F α ℝ]
[AddGroup α]
[AddGroupSeminormClass F α ℝ]
[inst : Dist α]
{f : F}
(hna : IsNonarchimedean ⇑f)
(hd : inst = PseudoMetricSpace.toDist := by rfl)
:

Proves that when a `SeminormedAddGroup`

structure is constructed from an
`AddGroupSeminormClass`

that satifies `IsNonarchimedean`

, the group has an `IsUltrametricDist`

.