wittAdd_zero — Mathlib

English

The Witt addition at index 0 is the sum of the zero-th coordinates: wittAdd p 0 = X(0,0) + X(1,0).

Русский

Сложение Witt на индексе 0 равно сумме нулевых координат: wittAdd p 0 = X(0,0) + X(1,0).

LaTeX

$$$$ \mathrm{wittAdd}(p,0) = X(0,0) + X(1,0). $$$$

Lean4

@[simp]
theorem wittAdd_zero : wittAdd p 0 = X (0, 0) + X (1, 0) :=
  by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittAdd, wittStructureRat, map_add, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, bind₁_X_right,
    map_wittStructureInt]

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