norm_nsmul — Mathlib

English

For any natural n and x in a NormedSpace E, the norm is homogeneous: ‖n • x‖ = n • ‖x‖.

Русский

Для любого натурального n и вектора x в нормированном пространстве E выполняется: ‖n · x‖ = n · ‖x‖.

LaTeX

$$$$\| n \cdot x \| = n \cdot \| x \|.$$$$

Lean4

theorem norm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖ = n • ‖x‖ := by
  simpa [Nat.cast_smul_eq_nsmul] using norm_smul (n : K) x

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