p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.160515
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (↑(map (Int.castRingHom R)) (W_ ℤ n)) ⊆ vars (W_ ℤ n)
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.160515
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (W_ R n) ⊆ range (n + 1)
rw [← map_wittPolynomial p (Int.castRingHom R), ← wittPolynomial_vars p ℤ]
no goals
p : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : DecidableEq R
S : Type ?u.160515
inst✝ : CommRing S
hp : NeZero p
n : ℕ
⊢ vars (↑(map (Int.castRingHom R)) (W_ ℤ n)) ⊆ vars (W_ ℤ n)
apply vars_map