hammingNorm_smul_le_hammingNorm — Mathlib

English

If 0 ≠ k and x is a vector, then the Hamming norm of k•x is bounded by the Hamming norm of x, provided the scalar algebra is compatible with zeros.

Русский

Если скаляр не нулевой и x — вектор, норма Хэмминга от k·x не превышает норму x, при условии совместимости нулей.

LaTeX

$$$hammingNorm (k \cdot x) \le hammingNorm x$$$

Lean4

theorem hammingNorm_smul_le_hammingNorm [Zero α] [∀ i, SMulWithZero α (β i)] {k : α} {x : ∀ i, β i} :
    hammingNorm (k • x) ≤ hammingNorm x :=
  hammingNorm_comp_le_hammingNorm (fun i (c : β i) => k • c) fun i => by simp_rw [smul_zero]

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