case a
σ : Type u_1
τ : Type ?u.7855
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x)) = ↑(↑(algebraMap R { x // x ∈ supported R s }) x)
σ : Type u_1
τ : Type ?u.7855
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x) = ↑(algebraMap R { x // x ∈ supported R s }) x
ext1
no goals
case a
σ : Type u_1
τ : Type ?u.7855
R : Type u
S : Type v
r : R
e : ℕ
n m : σ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
s : Set σ
x : R
⊢ ↑(↑(AlgEquiv.symm (supportedEquivMvPolynomial s)) (↑C x)) = ↑(↑(algebraMap R { x // x ∈ supported R s }) x)
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]