σ : Type u_1
τ : Type ?u.560
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ AlgHom.range (aeval fun x => X ↑x) = AlgHom.range (aeval (X ∘ Subtype.val))
σ : Type u_1
τ : Type ?u.560
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ supported R s = AlgHom.range (rename Subtype.val)
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]
no goals
σ : Type u_1
τ : Type ?u.560
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
⊢ AlgHom.range (aeval fun x => X ↑x) = AlgHom.range (aeval (X ∘ Subtype.val))
congr