instFintypeSymOfDecidableEq

Mathlib.Data.Fintype.Vector

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

English

Instance: if α is a finite type with DecidableEq, then the type Sym α n is finite.

Русский

Если α конечно и DecidableEq, то Sym α n конечно.

LaTeX

$$$$\\text{Finite}(\\mathrm{Sym}(\\alpha,n)).$$$$

Lean4

instance [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym α n) :=
  Fintype.ofEquiv _ Sym.symEquivSym'.symm

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

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

Разделы

Аффилиация

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