nonUnitalNormedCommRing — Mathlib

English

If α and β are nonunital normed commutative rings, their product α × β carries a nonunital normed commutative ring structure with the sup norm.

Русский

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

LaTeX

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

Lean4

/-- Non-unital normed commutative ring structure on the product of two non-unital normed
commutative rings, using the sup norm. -/
instance nonUnitalNormedCommRing [NonUnitalNormedCommRing β] : NonUnitalNormedCommRing (α × β) :=
  { Prod.nonUnitalSeminormedCommRing, Prod.normedAddCommGroup with }

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