English
If f: R → S is an injective nonunital ring homomorphism from a division ring R into a normed division ring S, then R carries a NormedDivisionRing structure obtained by pulling back the norm along f. Specifically, the induced norm ‖x‖_R is defined by ‖f(x)‖_S, and the multiplicative norm satisfies ‖xy‖_R = ‖f(x)‖_S · ‖f(y)‖_S.
Русский
Пусть f: R → S — инъективное негомоморфизм по умножению между делительным кольцом R и нормированным кольцом S. Тогда на R можно наделить структуру NormedDivisionRing, которая получается из нормы S через f: ‖x‖_R = ‖f(x)‖_S и ‖xy‖_R = ‖f(x)‖_S · ‖f(y)‖_S.
LaTeX
$$$\exists \|\cdot\|_R : R \to \mathbb{R}_{\ge 0} \text{ such that } (\forall x,y \in R),\; \|xy\|_R = \|f(x)\|_S \cdot \|f(y)\|_S \text{ and } \|x\|_R = \|f(x)\|_S.$$$
Lean4
/-- An injective non-unital ring homomorphism from a `DivisionRing` to a `NormedRing` induces a
`NormedDivisionRing` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [DivisionRing R] [NormedDivisionRing S] [NonUnitalRingHomClass F R S] (f : F)
(hf : Function.Injective f) : NormedDivisionRing R :=
{ NormedAddCommGroup.induced R S f hf, ‹DivisionRing R› with
norm_mul x y := show ‖f _‖ = _ from (map_mul f x y).symm ▸ norm_mul (f x) (f y) }
