wittPolynomial_eq_sum_C_mul_X_pow

English

Let p be a natural number and R a commutative ring. For every n, the Witt polynomial W_p,R,n expands as a finite sum over i = 0 to n of the coefficients C((p^i)) multiplied by X_i^{p^{n−i}}; i.e., W_p,R,n = sum_{i=0}^n C((p)^i) X_i^{p^{n−i}}.

Русский

Пусть p — натуральное число, R — коммутативный кольцо. Для любого n полином Witt удовлетворяет разложению: W_p,R,n = ∑_{i=0}^n C((p)^i) X_i^{p^{n−i}}.

LaTeX

$$$ wittPolynomial\ p\ R\ n = \sum_{i=0}^{n} C((p : R)^i) \; X_i^{p^{\,(n-i)}} $$$

Lean4

theorem wittPolynomial_eq_sum_C_mul_X_pow (n : ℕ) :
    wittPolynomial p R n = ∑ i ∈ range (n + 1), C ((p : R) ^ i) * X i ^ p ^ (n - i) :=
  by
  apply sum_congr rfl
  rintro i -
  rw [monomial_eq, Finsupp.prod_single_index]
  rw [pow_zero]

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