toHamming_symm_eq

Mathlib.InformationTheory.Hamming

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

English

The inverse of the toHamming equivalence equals the inverse map toHamming.symm = ofHamming.

Русский

Обратное отображение эквивалентности тоHamming совпадает с ofHamming.symm.

LaTeX

$$$(\mathrm{toHamming})^{-1} = \mathrm{ofHamming}$$$

Lean4

@[simp]
theorem toHamming_symm_eq : (@toHamming _ β).symm = ofHamming :=
  rfl

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

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

Разделы

Аффилиация

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