seminormedCommRing — Mathlib

English

If α and β are seminormed commutative rings, their product α × β has a seminormed commutative ring structure with the sup norm.

Русский

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

LaTeX

$$$\text{Prod }(\alpha,\beta) \text{ is a SeminormedCommRing with } \| (a,b) \| = \max\{ \|a\|, \|b\| \}$$$

Lean4

/-- Seminormed commutative ring structure on the product of two seminormed commutative rings,
  using the sup norm. -/
instance seminormedCommRing [SeminormedCommRing β] : SeminormedCommRing (α × β) :=
  { Prod.nonUnitalSeminormedCommRing, instCommRing with }

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