Hamming

Mathlib.InformationTheory.Hamming

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

Lean4

/-- Type synonym for a Pi type which inherits the usual algebraic instances, but is equipped with
the Hamming metric and norm, instead of `Pi.normedAddCommGroup` which uses the sup norm. -/
def Hamming {ι : Type*} (β : ι → Type*) : Type _ :=
  ∀ i, β i

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

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

Разделы

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

Аффилиация

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