instNormSMulClass — Mathlib

English

For a finite index set ι, and families β i, if each β i carries a NormSMulClass by α, then the product space Π i, β i carries a canonical NormSMulClass α.

Русский

Для конечного индекса ι и семейства β i, если каждое β i имеет NormSMulClass α, то произведение Π i, β i имеет канонический NormSMulClass α.

LaTeX

$$$NormSMulClass\\;α\\;\\left(\\Pi i,\\beta i\\right)$$$

Lean4

instance instNormSMulClass {ι : Type*} {β : ι → Type*} [Fintype ι] [SeminormedRing α] [∀ i, SeminormedAddGroup (β i)]
    [∀ i, SMul α (β i)] [∀ i, NormSMulClass α (β i)] : NormSMulClass α (Π i, β i) where
  norm_smul r x := by simp [nnnorm_def, ← coe_nnnorm, nnnorm_smul, ← NNReal.coe_mul, NNReal.mul_finset_sup]

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