norm_mkPiRing — Mathlib

English

The NN-norm of the SmulRight action satisfies a clean multiplicativity: the NN-norm of f.smulRight z equals the product of the NN-norm of f and that of z. This is the NNReal version of the SmulRight norm formula.

Русский

NN-норма f.smulRight z равна произведению NN-норf f и NN-норz.

LaTeX

$$$\|f\!\cdot\! z\|_{\mathrm{nn}} = \|f\|_{\mathrm{nn}} \cdot \|z\|_{\mathrm{nn}}$$$

Lean4

@[simp]
theorem norm_mkPiRing (z : G) : ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖ := by
  rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]

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