English
Let S be a subring of a normed ring R, and suppose R has a NormMulClass; then the induced norm on S (via the subtype map) makes S a NormMulClass as well, i.e. the norm is multiplicative on S relative to the induced structure.
Русский
Пусть S — подполье нормированного кольца R, и у R есть индуцированная норма и умножение; тогда индуцированная норма на S делает S нормированным кольцом с сохраняемостью умножения.
LaTeX
$$$\\text{If } S\\subseteq R \\text{ and } R \\text{ has a multiplicative norm } \\|\\cdot\\|, \\text{ then } S \\text{ with the induced norm satisfies } \\|xy\\| \\le \\|x\\|\\|y\\| \\text{ for all } x,y\\in S.$$$
Lean4
instance toNormMulClass [SeminormedRing R] [NormMulClass R] [SubringClass S R] (s : S) : NormMulClass s :=
.induced s R <| SubringClass.subtype _
