normedCommGroup — Mathlib

English

If each G_i is a NormedCommGroup and ι is finite, then the product ∏_i G_i, with the sup-norm, is a NormedCommGroup.

Русский

Если каждый G_i — нормированная коммутативная группа, то их произведение с суп-нормой образует NormedCommGroup.

LaTeX

$$Finite product of normed commutative groups, using the sup norm.$$

Lean4

/-- Finite product of normed groups, using the sup norm. -/
@[to_additive /-- Finite product of seminormed groups, using the sup norm. -/
    ]
instance normedCommGroup [∀ i, NormedCommGroup (G i)] : NormedCommGroup (∀ i, G i) :=
  { Pi.seminormedGroup with
    mul_comm := mul_comm
    eq_of_dist_eq_zero := eq_of_dist_eq_zero }

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