norm_smul — Mathlib

English

There is a standard construction turning a NormSMulClass structure into a NormSMulClass for a product-type, via a suitable norm on Π i, β i.

Русский

Существует стандартное построение перехода структуры NormSMulClass в NormSMulClass для произведения, используя норму на Π i, β i.

LaTeX

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

Lean4

theorem norm_smul [Norm α] [Norm β] [SMul α β] [NormSMulClass α β] (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖ :=
  NormSMulClass.norm_smul r x

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