WittVector.peval_polyOfInterest'

theorem WittVector.peval_polyOfInterest' : ∀ (p : ℕ) [hp : Fact p.Prime] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ) (x y : WittVector p k), WittVector.peval (WittVector.polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

This theorem, `WittVector.peval_polyOfInterest'`, establishes a relationship between the evaluation of a specific polynomial and certain operations on WittVectors in characteristic `p`, where `p` is a prime number. Specifically, given a commutative ring `k` of characteristic `p` and WittVectors `x` and `y` over `k`, for any natural number `n`, the theorem states that evaluating the polynomial of interest at a function mapping to the coefficients of `x` and `y` is equal to the coefficient of `x * y` at `n + 1` minus the `n + 1`-th power of `x.coeff 0` times `y.coeff (n + 1)` and minus the `n + 1`-th power of `y.coeff 0` times `x.coeff (n + 1)`.

More concisely: For a commutative ring of characteristic p and WittVectors x and y over it, the value of the polynomial of interest evaluated at the functions mapping to their coefficients is equal to the coefficient of x * y at n+1 minus the (n+1)-th power of x.coeff 0 * y.coeff (n+1) minus the (n+1)-th power of y.coeff 0 * x.coeff (n+1).