English
Given a functor-like F and a ring R with a seminormed target S, a nonunital ring homomorphism f: R → S induces a SeminormedRing structure on R via the pullback of norms along f.
Русский
При наличии отображения f: R → S с сохранением кольцевой структуры и семинорм на S, на R задаётся семинормированная кольцевая структура как обратное изображение нормы через f.
LaTeX
$$$\\text{SeminormedRing.induced}\\;R\\;S\\;f$$$
Lean4
/-- A non-unital ring homomorphism from a `Ring` to a `SeminormedRing` induces a
`SeminormedRing` structure on the domain.
See note [reducible non-instances] -/
abbrev induced [Ring R] [SeminormedRing S] [NonUnitalRingHomClass F R S] (f : F) : SeminormedRing R :=
{ NonUnitalSeminormedRing.induced R S f, SeminormedAddCommGroup.induced R S f, ‹Ring R› with }
