hammingDist_eq_hammingNorm — Mathlib

English

If each fiber is an additive group, then the Hamming distance equals the norm of the difference: hammingDist x y = hammingNorm(x − y).

Русский

Если каждый элемент пространства образует аддитивную группу, то расстояние Хэмминга равно норме разности: hammingDist x y = hammingNorm(x − y).

LaTeX

$$$hammingDist x y = hammingNorm (x - y)$$$

Lean4

/-- Corresponds to `dist_eq_norm`. -/
theorem hammingDist_eq_hammingNorm [∀ i, AddGroup (β i)] (x y : ∀ i, β i) : hammingDist x y = hammingNorm (x - y) := by
  simp_rw [hammingNorm, hammingDist, Pi.sub_apply, sub_ne_zero]

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