σ : Type u_1
τ : Type u_3
α : Type ?u.1038465
R : Type u_2
S : Type ?u.1038471
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) (support p)
σ : Type u_1
τ : Type u_3
α : Type ?u.1038465
R : Type u_2
S : Type ?u.1038471
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (↑(rename f) p) = Finset.image (Finsupp.mapDomain f) (support p)
rw [rename_eq]
no goals
σ : Type u_1
τ : Type u_3
α : Type ?u.1038465
R : Type u_2
S : Type ?u.1038471
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) (support p)
exact Finsupp.mapDomain_support_of_injective (mapDomain_injective h) _