English
If F: R → S is an injective nonunital ring homomorphism and S is a NormedRing, then R can be endowed with a NormedRing structure via the induced construction.
Русский
Если F: R → S — инъективный неаддитивный кольцевой гомоморфизм, и S — NormedRing, то R можно наделить структурой NormedRing через индуцированную конструкцию.
LaTeX
$$$\\text{NormedRing.induced}\\;R\\;S\\;F\\;\\text{(инъективен)}$$$
Lean4
/-- A non-unital ring homomorphism from a `NonUnitalCommRing` to a `NonUnitalSeminormedCommRing`
induces a `NonUnitalSeminormedCommRing` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [NonUnitalCommRing R] [NonUnitalSeminormedCommRing S] [NonUnitalRingHomClass F R S] (f : F) :
NonUnitalSeminormedCommRing R :=
{ NonUnitalSeminormedRing.induced R S f, ‹NonUnitalCommRing R› with }
