mk

Mathlib.RingTheory.WittVector.Truncated

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

English

The constructor mk sends a function x : Fin n → R to a truncated Witt vector.

Русский

Конструктор mk преобразует функцию x : Fin n → R в усечённый Witt-вектор.

LaTeX

$$$\\mathrm{mk}\\; p\\; x = x$$$

Lean4

/-- Create a `TruncatedWittVector` from a vector `x`. -/
def mk (x : Fin n → R) : TruncatedWittVector p n R :=
  x

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

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

Разделы

Аффилиация

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