English
For positive indices, the Witt unit vanishes: wittOne p n = 0 for n > 0.
Русский
Для положительных индексов единица по Witt-вектору обнуляется: wittOne p n = 0 при n > 0.
LaTeX
$$$$ \forall n>0,\; wittOne(p,n)=0. $$$$
Lean4
@[simp]
theorem wittOne_pos_eq_zero (n : ℕ) (hn : 0 < n) : wittOne p n = 0 :=
by
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
simp only [wittOne, wittStructureRat, RingHom.map_zero, map_one, map_wittStructureInt]
induction n using Nat.strong_induction_on with
| h n IH => ?_
rw [xInTermsOfW_eq]
simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right, bind₁_C_right]
rw [sub_mul, one_mul]
rw [Finset.sum_eq_single 0]
· simp only [invOf_eq_inv, one_mul, tsub_zero, pow_zero]
simp only [one_pow, one_mul, xInTermsOfW_zero, sub_self, bind₁_X_right]
· intro i hin hi0
rw [Finset.mem_range] at hin
rw [IH _ hin (Nat.pos_of_ne_zero hi0), zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero]
· grind
