constantCoeff — Mathlib

English

The coefficient at index 0 defines a ring hom from Witt vectors to the base ring: it sends a Witt vector to its 0-th coefficient.

Русский

Коэффициент при индексе 0 задаёт кольцевой гомоморф из Witt вектора в базовое кольцо: он отправляет вектор Уитта в его нулевой компонент.

LaTeX

$$$$ \text{constantCoeff}: \mathbb{W}_p(R) \to+* R, \quad \text{toFun}(x)=x_0. $$$$

Lean4

/-- `WittVector.coeff x 0` as a `RingHom` -/
@[simps]
noncomputable def constantCoeff : 𝕎 R →+* R where
  toFun x := x.coeff 0
  map_zero' := by simp
  map_one' := by simp
  map_add' := add_coeff_zero
  map_mul' := mul_coeff_zero

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