English
An injective non-unital ring homomorphism from a CommRing to a NormedRing induces a NormedCommRing structure on the domain.
Русский
Инъективный неаддитивный гомоморфизм от коммутативного кольца к NormedRing индуцирует NormedCommRing на область определения.
LaTeX
$$$\\text{NormedCommRing.induced}\\;R\\;S\\;f\\;\\text{(инъективен)}$$$
Lean4
/-- An injective non-unital ring homomorphism from a `CommRing` to a `NormedRing` induces a
`NormedCommRing` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [CommRing R] [NormedRing S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Injective f) :
NormedCommRing R :=
{ SeminormedCommRing.induced R S f, NormedAddCommGroup.induced R S f hf with }
