English
If f: E → F is a monoid homomorphism that is injective and F is a normed group, then E is equipped with a NormedGroup structure by pulling back the norm via f: ‖x‖_E := ‖f(x)‖_F and d_E(x,y) := d_F(f(x), f(y)).
Русский
Если f: E → F — гомоморфизм моноида, инъективен и F — нормированная группа, то E получает структуру NormedGroup путём вытягивания нормы через f: ‖x‖_E := ‖f(x)‖_F и d_E(x,y) := d_F(f(x), f(y)).
LaTeX
$$$\\|x\\|_E := \\|f(x)\\|_F \\quad\\text{and}\\quad d_E(x,y) = d_F(f(x), f(y))$$$
Lean4
/-- A group homomorphism from a `CommGroup` to a `SeminormedGroup` induces a
`SeminormedCommGroup` structure on the domain. -/
@[to_additive /-- A group homomorphism from an `AddCommGroup` to a
`SeminormedAddGroup` induces a `SeminormedAddCommGroup` structure on the domain. -/
]
abbrev induced [CommGroup E] [SeminormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) : SeminormedCommGroup E :=
{ SeminormedGroup.induced E F f with mul_comm := mul_comm }
-- See note [reducible non-instances].
