σ : Type u_1
R : Type u_3
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ↑(RingHom.comp (map σ (algebraMap R A)) (C σ R)) r = ↑(C σ A) (↑(algebraMap R A) r)
σ : Type u_1
R : Type u_3
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ↑(algebraMap R (MvPowerSeries σ A)) r = ↑(C σ A) (↑(algebraMap R A) r)
change (MvPowerSeries.map σ (algebraMap R A)).comp (C σ R) r = _
no goals
σ : Type u_1
R : Type u_3
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ↑(RingHom.comp (map σ (algebraMap R A)) (C σ R)) r = ↑(C σ A) (↑(algebraMap R A) r)
simp