instFintypeUnitsOfDecidableEq

Mathlib.Data.Fintype.Units

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

English

If α is a finite, with decidable equality, then the type of Sym(α,n) is finite.

Русский

Если у α конечный и существует разрешимое равенство, то тип Sym(α,n) конечно.

LaTeX

$$$$|\\mathrm{Sym}(\\alpha,n)| < \\infty.$$$$

Lean4

instance [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ :=
  Fintype.ofEquiv _ (unitsEquivProdSubtype α).symm

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

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

Разделы

Аффилиация

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