toList_formPerm_nil

Mathlib.GroupTheory.Perm.Cycle.Concrete

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.toList_formPerm_nil

English

The toList of a formPerm built from an empty list is empty for any x.

Русский

toList формPerm, построенный из пустого списка, пуст для любого x.

LaTeX

$$$$\forall x,\ toList(\mathrm{formPerm}([]:List\alpha))\ x = [].$$$$

Lean4

theorem toList_formPerm_nil (x : α) : toList (formPerm ([] : List α)) x = [] := by simp

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

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

Разделы

Аффилиация

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