instNormSMulClass — Mathlib

English

The product type β × γ carries a natural NormSMulClass α; the smul is defined componentwise with the product norm.

Русский

Произведение β × γ имеет естественную NormSMulClass α; умножение выполняется по компонентам с нормой на произведении.

LaTeX

$$$NormSMulClass\\;α\\;\\left(β \\times γ\\right)$$$

Lean4

instance instNormSMulClass {γ : Type*} [SeminormedAddGroup γ] [SMul α γ] [NormSMulClass α γ] : NormSMulClass α (β × γ)
    where
  norm_smul := fun r ⟨v₁, v₂⟩ ↦ by
    simp only [smul_def, ← coe_nnnorm, nnnorm_def, nnnorm_smul r, ← NNReal.coe_mul, NNReal.mul_sup]

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