aeval_wittPolynomial — Mathlib

English

Let A be a commutative ring and f: ℕ → A. Then aeval f (W_R n) equals the finite sum ∑_{i=0}^n (p^i) f(i)^{p^{n−i}} in A.

Русский

Пусть A — коммутативное кольцо и f: ℕ → A. Тогда aeval_f(W_R n) равно конечной сумме ∑_{i=0}^n p^i f(i)^{p^{n−i}} в A.

LaTeX

$$$ aeval\ f\ (W_R\ n) = \sum_{i=0}^{n} (p\,^{i}) \cdot f(i)^{p^{\,(n-i)}} $$$

Lean4

theorem aeval_wittPolynomial {A : Type*} [CommRing A] [Algebra R A] (f : ℕ → A) (n : ℕ) :
    aeval f (W_ R n) = ∑ i ∈ range (n + 1), (p : A) ^ i * f i ^ p ^ (n - i) := by
  simp [wittPolynomial, map_sum, aeval_monomial, Finsupp.prod_single_index]

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