instNeg

Mathlib.RingTheory.WittVector.Defs

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

English

The Witt vectors 𝕎_p(R) carry a negation operation, giving an additive group structure. The negation is defined by -x = eval (wittNeg p) (![x]).

Русский

Witt-вектора 𝕎_p(R) образуют группу по сложению, с операцией отрицания: -x = eval (wittNeg p) (![x]).

LaTeX

$$$$ -x = \mathrm{eval}\big(\mathrm{wittNeg}(p)\big)(![x]). $$$$

Lean4

instance : Neg (𝕎 R) :=
  ⟨fun x => eval (wittNeg p) ![x]⟩

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

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

Разделы

Аффилиация

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