cycleIcc_def_gt

Mathlib.GroupTheory.Perm.Fin

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

English

If i > j, then cycleIcc i j is the identity permutation.

Русский

Если i > j, то cycleIcc i j является тождественной перестановкой.

LaTeX

$$$cycleIcc(j,i) = 1$ при $i > j$$$

Lean4

@[simp]
theorem cycleIcc_def_gt (hij : i < j) : cycleIcc j i = 1 := by simp [cycleIcc, hij]

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

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

Разделы

Аффилиация

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