normedCommRing — Mathlib

English

If α and β are normed commutative rings, then α × β is a normed commutative ring with the sup norm.

Русский

Если α и β — нормированные коммутативные кольца, их произведение образует нормированное коммутативное кольцо с верхней нормой.

LaTeX

$$$\| (a,b) \|_{\infty} = \max\{ \|a\|, \|b\| \}$ and the product operations are coordinatewise.$$

Lean4

/-- Normed commutative ring structure on the product of two normed commutative rings, using the sup
norm. -/
instance normedCommRing [NormedCommRing β] : NormedCommRing (α × β) :=
  { nonUnitalNormedRing, instCommRing with }

Похожие утверждения