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