sign_swap'

Mathlib.GroupTheory.Perm.Sign

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

← MathLib Explorer

English

sign(swap x y) = -1 whenever x ≠ y.

Русский

sign(swap x y) = -1 при x ≠ y.

LaTeX

$$$\forall x,y,\ x \neq y \to \mathrm{sign}(\mathrm{swap}(x,y)) = -1$$$

Lean4

@[simp]
theorem sign_swap' {x y : α} : sign (swap x y) = if x = y then 1 else -1 :=
  if H : x = y then by simp [H, swap_self] else by simp [sign_swap H, H]

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

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

Разделы

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

Аффилиация

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