fintypePerm

Mathlib.Data.Fintype.Perm

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

← MathLib Explorer

English

The collection of permutations of a fintype α forms a fintype.

Русский

Множество перестановок конечного типа α образует конечный тип.

LaTeX

$$$[Fintype \\alpha] \\Rightarrow Fintype (Perm(\\alpha)).$$$

Lean4

/-- The collection of permutations of a fintype is a fintype. -/
def fintypePerm [Fintype α] : Fintype (Perm α) :=
  ⟨permsOfFinset (@Finset.univ α _), by simp [mem_perms_of_finset_iff]⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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