revPerm_symm

Mathlib.Data.Fin.Rev

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

English

The inverse of revPerm is itself; revPerm is symmetric under taking inverse.

Русский

Обратное к revPerm равно самому revPerm; revPerm симметрично относительно взятия обратного.

LaTeX

$$$(\mathrm{revPerm}_{n})^{-1} = \mathrm{revPerm}_{n}.$$$

Lean4

@[simp]
theorem revPerm_symm : (@revPerm n).symm = revPerm :=
  rfl

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

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

Разделы

Аффилиация

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