sign_symm

Mathlib.GroupTheory.Perm.Sign

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

English

sign(e.symm) = sign(e) for any permutation e.

Русский

sign(e.symm) = sign(e) для любой перестановки e.

LaTeX

$$$\forall e \in \mathrm{Perm}(\alpha),\ \mathrm{sign}(e^{-1}) = \mathrm{sign}(e)$$$

Lean4

@[simp]
theorem sign_symm (e : Perm α) : sign e.symm = sign e :=
  sign_inv e

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

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

Разделы

Аффилиация

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