mul_coeff_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_coeff_zero (x y : 𝕎 R) : (x * y).coeff 0 = x.coeff 0 * y.coeff 0 := by
  simp [mul_coeff, peval, Function.uncurry]

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