ofScalars_norm — Mathlib

English

If the field is normed with a norm-one space on E, then the norm of the nth coefficient equals the norm of c(n): ||ofScalars E c n|| = ||c(n)||.

Русский

Если пространство E нормировано с нормой единицы, то норма n-го коэффициента равна норме c(n): ||ofScalars E c n|| = ||c(n)||.

LaTeX

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

Lean4

@[simp]
theorem ofScalars_norm [NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖ := by simp [ofScalars_norm_eq_mul]

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