hammingNorm_smul — Mathlib

English

If the scalar acts regularly on every fiber, then hammingNorm(k•x) = hammingNorm(x).

Русский

Если действие скаляра на каждом срезе регуляривно, то вес сохраняется: hammingNorm(k·x) = hammingNorm(x).

LaTeX

$$$\forall i, \mathrm{IsSMulRegular}(\beta i)\ k \Rightarrow hammingNorm (k \cdot x) = hammingNorm x$$$

Lean4

theorem hammingNorm_smul [Zero α] [∀ i, SMulWithZero α (β i)] {k : α} (hk : ∀ i, IsSMulRegular (β i) k) (x : ∀ i, β i) :
    hammingNorm (k • x) = hammingNorm x :=
  hammingNorm_comp (fun i (c : β i) => k • c) hk fun i => by simp_rw [smul_zero]

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