cycleRange_symm_succ

Mathlib.GroupTheory.Perm.Fin

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

English

For i in Fin(n+1) and j in Fin n, i.cycleRange.symm(j.succ) = i.succAbove(j).

Русский

Для i ∈ Fin(n+1) и j ∈ Fin n, i.cycleRange.symm(j.succ) = i.succAbove(j).

LaTeX

$$$i.cycleRange._{-1}(j.succ) = i.succAbove(j)$$$

Lean4

@[simp]
theorem cycleRange_symm_succ (i : Fin (n + 1)) (j : Fin n) : i.cycleRange.symm j.succ = i.succAbove j :=
  i.cycleRange.injective (by simp)

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

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

Разделы

Аффилиация

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