ofScalars_norm_le — Mathlib

English

For each n, the norm of the nth coefficient equals the product of norms: ||ofScalars E c n|| = ||c n|| · ||mkPiAlgebraFin 𝕜 n E||.

Русский

Для каждого n норма n-го коэффициента равна произведению норм: ||ofScalars E c n|| = ||c n|| · ||mkPiAlgebraFin 𝕜 n E||.

LaTeX

$$$\|\operatorname{ofScalars} E c n\| = \|c(n)\| \cdot \|\operatorname{mkPiAlgebraFin} 𝕜 n E\|$$

Lean4

theorem ofScalars_norm_le (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖ :=
  by
  simp only [ofScalars_norm_eq_mul]
  exact (mul_le_of_le_one_right (norm_nonneg _) (ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos hn))

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