instFintypeOfDecidableEq

Mathlib.InformationTheory.Hamming

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

English

Provided DecidableEq ι and Fintype ι and each β i finite, the Hamming type is finite: Fintype (Hamming β).

Русский

При наличии DecidableEq ι и конечности ι и каждого β i тип Хэмминга конечен: Fintype(Hamming β).

LaTeX

$$$Fintype \,(Hamming \beta)$$$

Lean4

instance [DecidableEq ι] [Fintype ι] [∀ i, Fintype (β i)] : Fintype (Hamming β) :=
  Pi.instFintype

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

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

Разделы

Аффилиация

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