English
For invertible p in R, bind₁ (W_ R) (xInTermsOfW p R n) = X_n for all n.
Русский
При обратимости p в R, bind₁ (W_R) (xInTermsOfW p R n) = X_n для всех n.
LaTeX
$$$ bind₁ (W_\ R) (xInTermsOfW\ p\ R\ n) = X_n $$$
Lean4
@[simp]
theorem bind₁_wittPolynomial_xInTermsOfW [Invertible (p : R)] (n : ℕ) : bind₁ (W_ R) (xInTermsOfW p R n) = X n :=
by
induction n using Nat.strongRecOn with
| ind n H => ?_
rw [xInTermsOfW_eq, map_mul, map_sub, bind₁_X_right, algHom_C, map_sum,
show X n = (X n * C ((p : R) ^ n)) * C ((⅟p : R) ^ n) by
rw [mul_assoc, ← C_mul, ← mul_pow, mul_invOf_self, one_pow, map_one, mul_one]]
congr 1
rw [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, tsub_self, pow_zero, pow_one, mul_comm (X n),
add_sub_assoc, add_eq_left, sub_eq_zero]
apply sum_congr rfl
intro i h
rw [mem_range] at h
rw [map_mul, map_pow (bind₁ _), algHom_C, H i h, algebraMap_eq]
