signAux_one

Mathlib.GroupTheory.Perm.Sign

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

← MathLib Explorer

English

The sign of the identity permutation on Fin n is 1.

Русский

Знак идентичной перестановки на Fin n равен 1.

LaTeX

$$$ \\mathrm{signAux}(1) = 1 $$$

Lean4

@[simp]
theorem signAux_one (n : ℕ) : signAux (1 : Perm (Fin n)) = 1 :=
  by
  unfold signAux
  conv => rhs; rw [← @Finset.prod_const_one _ _ (finPairsLT n)]
  exact Finset.prod_congr rfl fun a ha => if_neg (mem_finPairsLT.1 ha).not_ge

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

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

Разделы

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

Аффилиация

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