nonUnitalNormedRing — Mathlib

English

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

Русский

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

LaTeX

$$$\text{Prod }(\alpha,\beta) \text{ is a nonunital normed ring with } \| (a,b) \| = \max\{ \|a\|, \|b\| \}. $$$

Lean4

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

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