cycleRange_symm_zero

Mathlib.GroupTheory.Perm.Fin

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

English

For any n > 0, the inverse cycleRange sends 0 to i. Equivalently, i.cycleRange.symm(0) = i.

Русский

Для любого n>0, обратная cycleRange отправляет 0 в i. Иными словами, i.cycleRange.symm(0) = i.

LaTeX

$$$i.cycleRange_{-1}(0) = i$$$

Lean4

@[simp]
theorem cycleRange_symm_zero [NeZero n] (i : Fin n) : i.cycleRange.symm 0 = i :=
  i.cycleRange.injective (by simp)

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

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

Разделы

Аффилиация

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