bind₁_xInTermsOfW_wittPolynomial

English

For invertible p in R, bind₁ (xInTermsOfW p R) (W_ R k) = X k for all k.

Русский

При обратимости p в R выполняется bind₁ (xInTermsOfW p R) (W_R k) = X_k для всех k.

LaTeX

$$$ bind₁ (xInTermsOfW\ p\ R) (W_\ R\ k) = X_k $$$

Lean4

@[simp]
theorem bind₁_xInTermsOfW_wittPolynomial [Invertible (p : R)] (k : ℕ) : bind₁ (xInTermsOfW p R) (W_ R k) = X k :=
  by
  rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum]
  simp only [map_pow, map_mul, algHom_C, algebraMap_eq]
  rw [sum_range_succ_comm, tsub_self, pow_zero, pow_one, bind₁_X_right, mul_comm, ← C_pow, xInTermsOfW_aux]
  simp only [C_pow, bind₁_X_right, sub_add_cancel]

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