sign_trans_trans_symm

Mathlib.GroupTheory.Perm.Sign

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

← MathLib Explorer

English

sign trans trans symmetry: sign ( (e.trans f).trans e⁻¹ ) = sign f

Русский

знак перестановок при двойном сопряжении: sign((e.trans f).trans e⁻¹) = sign f

LaTeX

$$$\forall f,e,\ sign((e^{-1} f) e) = sign f$$$

Lean4

@[simp]
theorem sign_trans_trans_symm [DecidableEq β] [Fintype β] (f : Perm β) (e : α ≃ β) :
    sign ((e.trans f).trans e.symm) = sign f :=
  sign_symm_trans_trans f e.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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