wittOne_zero_eq_one — Mathlib

English

The Witt vector corresponding to one has its 0th component equal to 1: wittOne p 0 = 1.

Русский

Witt-вектор, соответствующий единице, имеет нулевой компонент равным 1: wittOne p 0 = 1.

LaTeX

$$$$ wittOne\ (p,0) = 1. $$$$

Lean4

@[simp]
theorem wittOne_zero_eq_one : wittOne p 0 = 1 :=
  by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittOne, wittStructureRat, xInTermsOfW_zero, map_one, bind₁_X_right, map_wittStructureInt]

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