revAt_invol

Mathlib.Algebra.Polynomial.Reverse

URI: https://scilib.ai/kg/mathlib#Polynomial.revAt_invol

English

For all N,i, applying revAt N twice yields the identity: (revAt N)(revAt N i) = i.

Русский

Для любых N и i двойное применение revAt N дает исходное значение: (revAt N)(revAt N i) = i.

LaTeX

$$$\\forall N,i:\\; (revAt N)(revAt N i)=i.$$$

Lean4

@[simp]
theorem revAt_invol {N i : ℕ} : (revAt N) (revAt N i) = i :=
  revAtFun_invol

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

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

Разделы

Аффилиация

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