English
Combining polyOfInterest with the remainder expressions, the subset relation for vars persists, reinforcing that pegged Witt-variables remain within the expected index set after factoring in remainders.
Русский
Сочетание polyOfInterest с остаточными выражениями сохраняет включение переменных в ожидаемое множество индексов после учета остатков.
LaTeX
$$$((polyOfInterest\ p\ n).vars) \subseteq univ \times\! range (n+1)$$$
Lean4
/-- The characteristic `p` version of `peval_polyOfInterest` -/
theorem peval_polyOfInterest' (n : ℕ) (x y : 𝕎 k) :
peval (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) :=
by
rw [peval_polyOfInterest]
have : (p : k) = 0 := CharP.cast_eq_zero k p
simp only [this, ne_eq, add_eq_zero, and_false, zero_pow, zero_mul, add_zero, not_false_eq_true, reduceCtorEq]
have sum_zero_pow_mul_pow_p (y : 𝕎 k) :
∑ x ∈ range (n + 1 + 1), (0 : k) ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1) := by
rw [Finset.sum_eq_single_of_mem 0] <;> simp +contextual
congr <;> apply sum_zero_pow_mul_pow_p
