Lean4
/-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance and the
pseudometric space structure from the seminorm properties. Note that in most cases this instance
creates bad definitional equalities (e.g., it does not take into account a possibly existing
`UniformSpace` instance on `E`). -/
@[to_additive /-- Construct a seminormed group from a seminorm, i.e., registering the pseudodistance
and the pseudometric space structure from the seminorm properties. Note that in most cases this
instance creates bad definitional equalities (e.g., it does not take into account a possibly
existing `UniformSpace` instance on `E`). -/
]
abbrev toSeminormedCommGroup [CommGroup E] (f : GroupSeminorm E) : SeminormedCommGroup E :=
{ f.toSeminormedGroup with mul_comm := mul_comm }
-- See note [reducible non-instances]
