wittNeg

Mathlib.RingTheory.WittVector.Defs

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

← MathLib Explorer

English

The polynomials describing negation in 𝕎R are given by wittNeg p = wittStructureInt p (−X0).

Русский

Полиномы, задающие отрицание в 𝕎R: wittNeg p = wittStructureInt p (−X0).

LaTeX

$$$\\mathrm{WittVector.wittNeg}(p) = wittStructureInt(p, -X_0)$$$

Lean4

/-- The polynomials used for defining the negation of the ring of Witt vectors. -/
def wittNeg : ℕ → MvPolynomial (Fin 1 × ℕ) ℤ :=
  wittStructureInt p (-X 0)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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