wittZero_eq_zero — Mathlib

English

The Witt vector corresponding to zero has all its coefficients equal to zero: wittZero p n = 0 for every n.

Русский

Witt-вектор, соответствующий нулю, имеет все коэффициенты равными нулю: wittZero p n = 0 для всех n.

LaTeX

$$$$ wittZero\ (p,n) = 0. $$$$

Lean4

@[simp]
theorem wittZero_eq_zero (n : ℕ) : wittZero p n = 0 :=
  by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittZero, wittStructureRat, bind₁, aeval_zero', constantCoeff_xInTermsOfW, map_zero, map_wittStructureInt]

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