toHamming_ofHamming

Mathlib.InformationTheory.Hamming

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

English

The map toHamming after applying ofHamming is the identity on Hamming β: toHamming (ofHamming x) = x.

Русский

Применение toHamming после ofHamming даёт тождественный отображение на Hamming β: toHamming (ofHamming x) = x.

LaTeX

$$$toHamming (ofHamming x) = x$$$

Lean4

@[simp]
theorem toHamming_ofHamming (x : Hamming β) : toHamming (ofHamming x) = x :=
  rfl

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

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

Разделы

Аффилиация

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