English
For any natural n and x in a NormedAddCommMonoid, the nnnorm is homogeneous: ‖n • x‖₊ = n • ‖x‖₊.
Русский
Для любого натурального n и x в нормированном аддитивном коммутативном моное выполняется: ‖n · x‖₊ = n · ‖x‖₊.
LaTeX
$$$$\| n \cdot x \|_{+} = n \cdot \| x \|_{+}.$$$$
Lean4
theorem nnnorm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) : ‖n • x‖₊ = n • ‖x‖₊ := by
simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x