swap_smul_involutive

Mathlib.GroupTheory.Perm.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.swap_smul_involutive

English

The map x ↦ swap(i,j) • x is an involution; applying it twice yields the identity map.

Русский

Карта x ↦ swap(i,j) • x является инволютивной; два подряд применения дают тождественную карту.

LaTeX

$$Function.Involutive (swap i j • ·)$$

Lean4

theorem swap_smul_involutive [MulAction (Perm α) β] (i j : α) : Function.Involutive (swap i j • · : β → β) :=
  swap_smul_self_smul i j

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

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

Разделы

Аффилиация

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