English
The finite product of non-unital normed commutative rings is itself a non-unital normed commutative ring under the sup norm.
Русский
Конченное произведение неединичных нормированных коммутативных колец образует неединичное нормированное коммутативное кольцо под суп-нормой.
LaTeX
$$$ \\prod_{i=1}^n R_i \\text{ is a non-unital normed commutative ring with } \\|x\\|_\\infty = \\max_i \\|x_i\\|.$$$
Lean4
instance (priority := 100) toContinuousMul [NonUnitalSeminormedRing α] : ContinuousMul α :=
⟨continuous_iff_continuousAt.2 fun x =>
tendsto_iff_norm_sub_tendsto_zero.2 <|
by
have : ∀ e : α × α, ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
by
intro e
calc
‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
rw [mul_sub, sub_mul, sub_add_sub_cancel]
_ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
refine squeeze_zero (fun e => norm_nonneg _) this ?_
convert
((continuous_fst.tendsto x).norm.mul ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
(((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul tendsto_const_nhds)
simp⟩
-- see Note [lower instance priority]
