hammingDist_zero_left

Mathlib.InformationTheory.Hamming

URI: https://scilib.ai/kg/mathlib#hammingDist_zero_left

← MathLib Explorer

English

The distance between the zero vector and x equals the Hamming weight of x.

Русский

Расстояние от нулевого вектора до x равно весу Хэмминга x.

LaTeX

$$$hammingDist 0 x = hammingNorm x$$$

Lean4

/-- Corresponds to `dist_zero_left`. -/
@[simp]
theorem hammingDist_zero_left : hammingDist (0 : ∀ i, β i) = hammingNorm :=
  funext fun x => by rw [hammingDist_comm, hammingDist_zero_right]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru