verschiebungFun_coeff_succ

Mathlib.RingTheory.WittVector.Verschiebung

URI: https://scilib.ai/kg/mathlib#WittVector.verschiebungFun_coeff_succ

English

For all x and n, the coefficient at n+1 of verschiebungFun x equals the coefficient at n of x.

Русский

Для всех x и n коэффициент при индексе n+1 в verschiebungFun x равен коэффициенту при индексе n в x.

LaTeX

$$$$ (\\\\text{verschiebungFun}(x))_{n+1} = x_{n}. $$$$

Lean4

@[simp]
theorem verschiebungFun_coeff_succ (x : 𝕎 R) (n : ℕ) : (verschiebungFun x).coeff n.succ = x.coeff n :=
  rfl

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

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

Разделы

Аффилиация

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