shift_coeff

Mathlib.RingTheory.WittVector.Domain

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

English

The shift property states that for all p and R, (x.shift n).coeff k = x.coeff(n+k).

Русский

Свойство сдвига утверждает, что для всех p и R, (x.shift n).coeff k = x.coeff(n+k).

LaTeX

$$$\big( x.shift\, n \big).\text{coeff } k = x.\text{coeff }(n+k)$$$

Lean4

theorem shift_coeff (x : 𝕎 R) (n k : ℕ) : (x.shift n).coeff k = x.coeff (n + k) :=
  rfl

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

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

Разделы

Аффилиация

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