ofHamming_neg

Mathlib.InformationTheory.Hamming

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

English

The inverse encoding respects negation: ofHamming(-x) = -ofHamming x.

Русский

Обратное кодирование сохраняет отрицание: ofHamming(-x) = -ofHamming x.

LaTeX

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

Lean4

@[simp]
theorem ofHamming_neg [∀ i, Neg (β i)] {x : Hamming β} : ofHamming (-x) = -ofHamming x :=
  rfl

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

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

Разделы

Аффилиация

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