sign_cycleRange

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Fin.sign_cycleRange

English

For any finite n and any i in Fin n, the sign of the permutation cycleRange i equals (−1) to the power i.

Русский

Для любого n и любого i в Fin n знак перестановки cycleRange i равен (−1) возрастом i.

LaTeX

$$$\operatorname{sign}(\operatorname{cycleRange}(i)) = (-1)^{i}$$$

Lean4

@[simp]
theorem sign_cycleRange (i : Fin n) : Perm.sign (cycleRange i) = (-1) ^ (i : ℕ) := by simp [cycleRange]

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

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

Разделы

Аффилиация

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