wittNeg_zero

Mathlib.RingTheory.WittVector.Defs

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

← MathLib Explorer

English

The Witt negation at index 0 is −X(0,0).

Русский

Отрицание Witt на индексе 0 равно −X(0,0).

LaTeX

$$$$ \mathrm{wittNeg}(p,0) = -X(0,0). $$$$

Lean4

@[simp]
theorem wittNeg_zero : wittNeg p 0 = -X (0, 0) :=
  by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittNeg, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, map_neg, bind₁_X_right,
    map_wittStructureInt]

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

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

Разделы

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

Аффилиация

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