English
If α and β are nonunital seminormed commutative rings, their product α × β inherits a nonunital seminormed commutative ring structure with the sup norm.
Русский
Если α и β — неединичные семинормированные коммутативные кольца, их произведение α × β наследует неединичную семинормированную коммутативную кольцевую структуру с верхней нормой.
LaTeX
$$$\text{Prod }(\alpha,\beta) \text{ is a nonUnital SeminormedCommRing with } \| (a,b) \| = \max\{ \|a\|, \|b\| \}$$$
Lean4
/-- Non-unital seminormed commutative ring structure on the product of two non-unital seminormed
commutative rings, using the sup norm. -/
instance nonUnitalSeminormedCommRing [NonUnitalSeminormedCommRing β] : NonUnitalSeminormedCommRing (α × β) :=
{ nonUnitalSeminormedRing, instNonUnitalCommRing with }
