no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.221880
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
hf : Injective ↑f
⊢ vars (↑(map f) p) = vars p
simp [vars, degrees_map_of_injective _ hf]