revAtFun_eq

Mathlib.Algebra.Polynomial.Reverse

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

English

The unbundled and bundled versions of revAtFun coincide, i.e., revAtFun N i = revAt N i.

Русский

Неупакованная и упакованная версии revAtFun совпадают: revAtFun N i = revAt N i.

LaTeX

$$$\\text{revAtFun}(N,i)=\\text{revAt}(N,i).$$$

Lean4

/-- We prefer to use the bundled `revAt` over unbundled `revAtFun`. -/
@[simp]
theorem revAtFun_eq (N i : ℕ) : revAtFun N i = revAt N i :=
  rfl

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

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

Разделы

Аффилиация

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