σ : Type ?u.4313394
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
a : R
this : ↑(↑(monomial 0) a) = ↑(PowerSeries.monomial R 0) a
⊢ ↑(↑C a) = ↑(PowerSeries.C R) a
σ : Type ?u.4313394
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
a : R
⊢ ↑(↑C a) = ↑(PowerSeries.C R) a
have := coe_monomial 0 a
no goals
σ : Type ?u.4313394
R : Type u_1
inst✝ : CommSemiring R
φ ψ : R[X]
a : R
this : ↑(↑(monomial 0) a) = ↑(PowerSeries.monomial R 0) a
⊢ ↑(↑C a) = ↑(PowerSeries.C R) a
rwa [PowerSeries.monomial_zero_eq_C_apply] at this