English
The induced NormedRing on R satisfies the usual norm axioms pulled back via the injective homomorphism F.
Русский
Индуцированное NormedRing на R удовлетворяет стандартным аксиомам нормы, вытянутым через инъективное отображение F.
LaTeX
$$$\\|\\cdot\\|_{R}=\\|F(\\cdot)\\|_{S}$ satisfies norm properties$$
Lean4
/-- An injective non-unital ring homomorphism from a `NonUnitalCommRing` to a
`NonUnitalNormedCommRing` induces a `NonUnitalNormedCommRing` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [NonUnitalCommRing R] [NonUnitalNormedCommRing S] [NonUnitalRingHomClass F R S] (f : F)
(hf : Function.Injective f) : NonUnitalNormedCommRing R :=
{ NonUnitalNormedRing.induced R S f hf, ‹NonUnitalCommRing R› with }
