coeff

Mathlib.RingTheory.WittVector.Truncated

URI: https://scilib.ai/kg/mathlib#TruncatedWittVector.coeff

English

The coefficient function retrieves the i-th component of a truncated Witt vector.

Русский

Функция коэффициента возвращает i-я компоненту усечённого Witt-вектора.

LaTeX

$$$\\mathrm{TruncatedWittVector}.\\mathrm{coeff}(i, x) = x(i)$$$

Lean4

/-- `x.coeff i` is the `i`th entry of `x`. -/
def coeff (i : Fin n) (x : TruncatedWittVector p n R) : R :=
  x i

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

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

Разделы

Аффилиация

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