norm_apply_eq_norm_coef — Mathlib

English

For a formal multilinear series p, the operator norm of the nth term p n equals the norm of the nth coefficient: ‖p n‖ = ‖coeff p n‖.

Русский

Для формальной мультилініейной серии p операторная норма n-го члена p n равна норме n-го коэффициента: ‖p n‖ = ‖coeff p n‖.

LaTeX

$$$\\|p\,n\\| = \\|\\mathrm{coeff}\\ p\\ n\\|$$$

Lean4

@[simp]
theorem norm_apply_eq_norm_coef : ‖p n‖ = ‖coeff p n‖ := by
  rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]

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