English
If f: E → F is an injective monoid homomorphism from a commutative group E to a normed group F, then E inherits a NormedCommGroup structure by pulling back the norm and keeping commutativity of multiplication.
Русский
Если f: E → F — инъективный моноид-гомоморфизм из коммутативной группы E в нормированную группу F, то E получает структуру NormedCommGroup путём вытягивания нормы и сохранения коммутативности умножения.
LaTeX
$$$\\text{Induced } E F f h: \\text{NormedCommGroup } E$$$
Lean4
/-- An injective group homomorphism from a `CommGroup` to a `NormedGroup` induces a
`NormedCommGroup` structure on the domain. -/
@[to_additive /-- An injective group homomorphism from a `CommGroup` to a
`NormedCommGroup` induces a `NormedCommGroup` structure on the domain. -/
]
abbrev induced [CommGroup E] [NormedGroup F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (h : Injective f) : NormedCommGroup E :=
{ SeminormedGroup.induced E F f, MetricSpace.induced f h _ with mul_comm := mul_comm }
