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