sign_cycleIcc_of_eq

Mathlib.GroupTheory.Perm.Fin

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

English

The sign of the cycleIcc(i,i) is 1.

Русский

Знак перестановки cycleIcc(i,i) равен 1.

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i : \\mathrm{Fin}(n)},\\; \\mathrm{Perm}.\\mathrm{sign}(\\mathrm{cycleIcc}(i,i)) = 1$$$

Lean4

theorem sign_cycleIcc_of_eq : Perm.sign (cycleIcc i i) = 1 := by
  rw [sign_cycleIcc_of_le (Fin.ge_of_eq rfl), tsub_self, pow_zero]

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

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

Разделы

Аффилиация

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