p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x in range (n + 1), ↑(map f) (↑(monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i in range (n + 1), ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ↑(map f) (W_ R n) = W_ S n
rw [wittPolynomial, map_sum, wittPolynomial]
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ↑(map f) (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n : ℕ
⊢ ∑ x in range (n + 1), ↑(map f) (↑(monomial (single x (p ^ (n - x)))) (↑p ^ x)) =
    ∑ i in range (n + 1), ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
refine sum_congr rfl fun i _ => ?_
no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ↑(map f) (↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)) = ↑(monomial (single i (p ^ (n - i)))) (↑p ^ i)
rw [map_monomial, RingHom.map_pow, map_natCast]