toHamming_neg

Mathlib.InformationTheory.Hamming

URI: https://scilib.ai/kg/mathlib#Hamming.toHamming_neg

English

The encoding commutes with negation: toHamming(-x) = -toHamming x.

Русский

Кодирование сохраняет отрицание: toHamming(-x) = -toHamming x.

LaTeX

$$$\\operatorname{toHamming}(-x) = -\\operatorname{toHamming} x$$$

Lean4

@[simp]
theorem toHamming_neg [∀ i, Neg (β i)] {x : ∀ i, β i} : toHamming (-x) = -toHamming x :=
  rfl

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

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

Разделы

Аффилиация

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