case hf
σ : Type u_1
τ : Type ?u.128090
R : Type u_2
S : Type ?u.128096
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ
⊢ ↑(expand 1) (X f) = ↑(AlgHom.id R (MvPolynomial σ R)) (X f)
σ : Type u_1
τ : Type ?u.128090
R : Type u_2
S : Type ?u.128096
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ expand 1 = AlgHom.id R (MvPolynomial σ R)
ext1 f
no goals
case hf
σ : Type u_1
τ : Type ?u.128090
R : Type u_2
S : Type ?u.128096
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ
⊢ ↑(expand 1) (X f) = ↑(AlgHom.id R (MvPolynomial σ R)) (X f)
rw [expand_one_apply, AlgHom.id_apply]