norm_units_zsmul — Mathlib

English

In a seminormed additive group, for any unit n ∈ ℤˣ and any a ∈ E, the norm is invariant under scalar multiplication by n: ‖n • a‖ = ‖a‖.

Русский

В аддитивной нормированной группе для любого единичного целого n и любого a выполняется ‖n • a‖ = ‖a‖.

LaTeX

$$$\forall a \in E,\ n \in \mathbb{Z}^{\times},\ \|n \cdot a\| = \|a\|$$$

Lean4

@[simp]
theorem norm_units_zsmul {E : Type*} [SeminormedAddGroup E] (n : ℤˣ) (a : E) : ‖n • a‖ = ‖a‖ :=
  norm_isUnit_zsmul a n.isUnit

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