instFintypeSym'OfDecidableEq

Mathlib.Data.Fintype.Vector

URI: https://scilib.ai/kg/mathlib#instFintypeSym'OfDecidableEq

English

The type Sym' α n is finite when α is finite and equality on α is decidable.

Русский

Тип Sym' α n конечно, если α конечно и равенство над α разрешимо.

LaTeX

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

Lean4

instance [DecidableEq α] [Fintype α] {n : ℕ} : Fintype (Sym.Sym' α n) :=
  Quotient.fintype _

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

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

Разделы

Аффилиация

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