English
If p is invertible in R, then xInTermsOfW p R n equals (X_n − ∑_{i=0}^{n-1} C(p^i) xInTermsOfW p R i^{p^{(n−i)}}) · C((p^{-1})^n).
Русский
Если p обратимо в R, то xInTermsOfW p R n равно (X_n − ∑_{i=0}^{n-1} C(p^i) xInTermsOfW p R i^{p^{(n−i)}}) · C((p^{-1})^n).
LaTeX
$$$ xInTermsOfW\ p\ R\ n = \bigl(X_n - \sum_{i=0}^{n-1} C((p : R)^i) \cdot xInTermsOfW\ p\ R\ i^{p^{(n-i)}}\bigr) \cdot C((p^{-1} : R)^n) $$$
Lean4
/-- The `xInTermsOfW p R n` is the polynomial on the basis of Witt polynomials
that corresponds to the ordinary `X n`. -/
noncomputable def xInTermsOfW [Invertible (p : R)] : ℕ → MvPolynomial ℕ R
| n => (X n - ∑ i : Fin n, C ((p : R) ^ (i : ℕ)) * xInTermsOfW i ^ p ^ (n - (i : ℕ))) * C ((⅟p : R) ^ n)
