add_coeff_zero — Mathlib

English

Let x and y be Witt vectors over R. The zeroth coefficient of their sum is the sum of their zeroth coefficients.

Русский

Пусть x и y — Witt-векторы над R. Нулевой коэффициент их суммы равен сумме нулевых коэффициентов.

LaTeX

$$$(x + y).\text{coeff } 0 = x.\text{coeff } 0 + y.\text{coeff } 0$$$

Lean4

theorem add_coeff_zero (x y : 𝕎 R) : (x + y).coeff 0 = x.coeff 0 + y.coeff 0 := by
  simp [add_coeff, peval, Function.uncurry]

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