English
The finite product of non-unital seminormed rings, endowed with the supremum norm, carries a natural non-unital seminormed ring structure.
Русский
Конечное произведение неединичных полей с сипонимормной структурой на норме имеет естественную структуру ненулевого полинормного кольца.
LaTeX
$$$ \\left( \\prod_{i=1}^n R_i, \\; \\|x\\|_\\infty \\right) \\text{ is a } \\text{non-unital seminormed ring with } \\|xy\\|_\\infty \\le \\|x\\|_\\infty \\|y\\|_\\infty.$$$
Lean4
/-- Non-unital seminormed ring structure on the product of finitely many non-unital seminormed
rings, using the sup norm. -/
instance nonUnitalSeminormedRing {R : ι → Type*} [Fintype ι] [∀ i, NonUnitalSeminormedRing (R i)] :
NonUnitalSeminormedRing (∀ i, R i) :=
{ seminormedAddCommGroup, nonUnitalRing with
norm_mul_le x
y :=
NNReal.coe_mono <|
calc
(univ.sup fun i ↦ ‖x i * y i‖₊) ≤ univ.sup ((‖x ·‖₊) * (‖y ·‖₊)) := sup_mono_fun fun _ _ ↦ nnnorm_mul_le _ _
_ ≤ (univ.sup (‖x ·‖₊)) * univ.sup (‖y ·‖₊) :=
sup_mul_le_mul_sup_of_nonneg (fun _ _ ↦ zero_le _) fun _ _ ↦ zero_le _ }
