instDecidableEqOfFintype

Mathlib.InformationTheory.Hamming

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

English

If ι is finite and each β i has DecidableEq, then DecidableEq (Hamming β).

Русский

Если ι конечен и каждый β i имеет DecidableEq, то DecidableEq(Hamming β).

LaTeX

$$[DecidableEq (Hamming β)]$$

Lean4

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

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

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

Разделы

Аффилиация

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