R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C)) x = ↑C x
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C) = C
refine' RingHom.ext fun x => _
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑↑(AlgEquiv.symm (finSuccEquiv R n)) (↑(RingHom.comp Polynomial.C C) x) = ↑C x
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp (↑(AlgEquiv.symm (finSuccEquiv R n))) (RingHom.comp Polynomial.C C)) x = ↑C x
rw [RingHom.comp_apply]
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp Polynomial.C C) x = ↑(finSuccEquiv R n) (↑C x)
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑↑(AlgEquiv.symm (finSuccEquiv R n)) (↑(RingHom.comp Polynomial.C C) x) = ↑C x
refine'
  (MvPolynomial.finSuccEquiv R n).injective
    (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) _)
no goals
R✝ : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.975050
a a' a₁ a₂ : R✝
e : ℕ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R✝
n✝ : ℕ
R : Type u
inst✝ : CommSemiring R
n : ℕ
x : R
⊢ ↑(RingHom.comp Polynomial.C C) x = ↑(finSuccEquiv R n) (↑C x)
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]