one_symm

Mathlib.Algebra.Group.End

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

English

The inverse of the identity permutation is the identity itself.

Русский

Обратная тождественной перестановки равна самой тождественной перестановке.

LaTeX

$$$\\\\bigl(1 : \\\\mathrm{Perm} \\\\alpha\\\\bigr)^{-1} = 1$$$

Lean4

@[simp]
theorem one_symm : (1 : Perm α).symm = 1 :=
  rfl

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

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

Разделы

Аффилиация

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