normedCommutativeRing — Mathlib

English

The finite product of normed commutative rings, with the sup-norm, is a NormedCommRing.

Русский

Конечное произведение нормированных коммутативных колец, с суп-нормой, образует NormedCommRing.

LaTeX

$$$ \\prod_{i=1}^n R_i \\text{ is a } \\text{NormedCommRing with sup-norm } \\|x\\|_\\infty = \\max_i \\|x_i\\|.$$$

Lean4

/-- Normed commutative ring structure on the product of finitely many normed commutative rings,
using the sup norm. -/
instance normedCommutativeRing {R : ι → Type*} [Fintype ι] [∀ i, NormedCommRing (R i)] : NormedCommRing (∀ i, R i) :=
  { Pi.seminormedCommRing, Pi.normedAddCommGroup with }

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