English
If f: R → S is an injective nonunital ring homomorphism from a field R into a NormedField S, then R inherits a NormedField structure by pulling back the NormedDivisionRing structure from S, with the multiplication being commutative.
Русский
Пусть f: R → S — инъективный негомиорфизм по умножению от поля R к нормированному полю S. Тогда R наследует структуру NormedField посредством взятия нормы через f и сохранения коммутативности умножения.
LaTeX
$$$\exists \|\cdot\|_R : R \to \mathbb{R}_{\ge 0},\; \forall x,y \in R:\; \|xy\|_R = \|f(x)\|_S \cdot \|f(y)\|_S \quad \text{and} \; \|x\|_R = \|f(x)\|_S,$ with multiplication commutative.$$
Lean4
/-- An injective non-unital ring homomorphism from a `Field` to a `NormedRing` induces a
`NormedField` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [Field R] [NormedField S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :
NormedField R :=
{ NormedDivisionRing.induced R S f hf with mul_comm := mul_comm }
