English
The finite product of non-unital seminormed commutative rings, with pointwise multiplication, forms a non-unital seminormed commutative ring under the sup-norm.
Русский
Конечное произведение неединичных полей коммутативных нормированных колец образует неединичное нормированное коммутативное кольцо при суп-норме.
LaTeX
$$$ \\prod_{i=1}^n R_i \\text{ carries a } \\text{NonUnitalSeminormedCommRing structure with } \\|x\\|_\\infty = \\max_i \\|x_i\\|_+.$$$
Lean4
/-- Seminormed commutative ring structure on the product of finitely many seminormed commutative
rings, using the sup norm. -/
instance seminormedCommRing {R : ι → Type*} [Fintype ι] [∀ i, SeminormedCommRing (R i)] :
SeminormedCommRing (∀ i, R i) :=
{ Pi.nonUnitalSeminormedCommRing, Pi.ring with }
