sign_refl

Mathlib.GroupTheory.Perm.Sign

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

English

sign(f^{-1}) = sign(f) for any permutation f.

Русский

sign(f^{-1}) = sign(f) для любой перестановки f.

LaTeX

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

Lean4

@[simp]
theorem sign_refl : sign (Equiv.refl α) = 1 :=
  MonoidHom.map_one sign

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

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

Разделы

Аффилиация

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