English
Let k act regularly on every fiber β i and x, y be elements of the product ∀ i, β i. Then the Hamming distance is preserved under the coordinatewise action by k: d_H(k·x, k·y) = d_H(x, y).
Русский
Пусть k действует регулярно на каждом ответвлении β i и x, y являются элементами произведения ∀ i, β i. Тогда расстояние Хэмминга сохраняется при поразрядном умножении на k: d_H(k·x, k·y) = d_H(x, y).
LaTeX
$$$hammingDist (k \cdot x) (k \cdot y) = hammingDist x y$$$
Lean4
/-- Corresponds to `dist_smul` with the discrete norm on `α`. -/
theorem hammingDist_smul [∀ i, SMul α (β i)] {k : α} {x y : ∀ i, β i} (hk : ∀ i, IsSMulRegular (β i) k) :
hammingDist (k • x) (k • y) = hammingDist x y :=
hammingDist_comp (fun i => (k • · : β i → β i)) hk
