p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑(monomial (single x (p ^ (n - x)))) (↑p ^ x) = ↑C (↑p ^ x) * X x ^ p ^ (n - x)
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ wittPolynomial p R n = ∑ i in range (n + 1), ↑C (↑p ^ i) * X i ^ p ^ (n - i)
apply sum_congr rfl
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i) = ↑C (↑p ^ i) * X i ^ p ^ (n - i)
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range (n + 1) → ↑(monomial (single x (p ^ (n - x)))) (↑p ^ x) = ↑C (↑p ^ x) * X x ^ p ^ (n - x)
rintro i -
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ X i ^ 0 = 1
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i) = ↑C (↑p ^ i) * X i ^ p ^ (n - i)
rw [monomial_eq, Finsupp.prod_single_index]
no goals
p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : DecidableEq R
n i : ℕ
⊢ X i ^ 0 = 1
rw [pow_zero]