English
Let p be prime and invertible in R; the constant coefficient of xInTermsOfW p R n is zero for all n.
Русский
Пусть p — простое и обратимо в R; константный коэффициент xInTermsOfW p R n равен нулю для всех n.
LaTeX
$$$ \operatorname{constantCoeff}(xInTermsOfW\ p\ R\ n) = 0 $$$
Lean4
@[simp]
theorem constantCoeff_xInTermsOfW [hp : Fact p.Prime] [Invertible (p : R)] (n : ℕ) :
constantCoeff (xInTermsOfW p R n) = 0 :=
by
induction n using Nat.strongRecOn with
| ind n IH => ?_
rw [xInTermsOfW_eq, mul_comm, RingHom.map_mul, RingHom.map_sub, map_sum, constantCoeff_C, constantCoeff_X, zero_sub,
mul_neg, neg_eq_zero, sum_eq_zero, mul_zero]
intro m H
rw [mem_range] at H
simp only [RingHom.map_mul, RingHom.map_pow, map_natCast, IH m H]
rw [zero_pow, mul_zero]
exact pow_ne_zero _ hp.1.ne_zero
