English
If α and β are normed rings, then their product α × β is a normed ring with the sup norm, defined analogously by ∥(a,b)∥∞ = max{∥a∥, ∥b∥}. The product operations are coordinatewise.
Русский
Если α и β — нормированные кольца, то их произведение α × β является нормированным кольцом с верхней нормой, заданной аналогично ∥(a,b)∥∞ = max{∥a∥, ∥b∥}. Операции делаются по координатам.
LaTeX
$$$\| (a,b) \|_{\infty} = \max\{ \|a\|, \|b\| \}$ and \(α × β\) is a NormedRing$$
Lean4
/-- Normed ring structure on the product of two normed rings, using the sup norm. -/
instance normedRing [NormedRing β] : NormedRing (α × β) :=
{ nonUnitalNormedRing, instRing with }
