σ : Type u_1
τ : Type u_3
α : Type ?u.345007
R : Type u_2
S : Type ?u.345013
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(killCompl hf) (↑(rename f) (X i)) = X i
σ : Type u_1
τ : Type u_3
α : Type ?u.345007
R : Type u_2
S : Type ?u.345013
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(AlgHom.comp (killCompl hf) (rename f)) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
dsimp
no goals
σ : Type u_1
τ : Type u_3
α : Type ?u.345007
R : Type u_2
S : Type ?u.345013
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(killCompl hf) (↑(rename f) (X i)) = X i
rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos, Equiv.ofInjective_symm_apply]