toList_formPerm_singleton

Mathlib.GroupTheory.Perm.Cycle.Concrete

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

English

The toList of the formPerm built from a singleton list [x] is empty for any y.

Русский

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

LaTeX

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

Lean4

theorem toList_formPerm_singleton (x y : α) : toList (formPerm [x]) y = [] := by simp

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

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

Разделы

Аффилиация

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