coeff_mk

Mathlib.RingTheory.WittVector.Defs

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

English

The nth coefficient of the Witt vector obtained from a sequence x is exactly x(n).

Русский

n‑й коэффициент Witt‑вектора, полученного из последовательности x, равен x(n).

LaTeX

$$$(\\mathrm{WittVector.mk}(p, x)).\\mathrm{coeff}(n) = x(n)$$$

Lean4

@[simp]
theorem coeff_mk (x : ℕ → R) : (mk p x).coeff = x :=
  rfl

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

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

Разделы

Аффилиация

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