case coeff.h
R : Type u
R' : Type ?u.298758
inst✝³ : Semiring R
inst✝² : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : PowerSeries S
x✝ : ℤ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ S) (r • x)) x✝ = HahnSeries.coeff (r • ↑(ofPowerSeries ℤ S) x) x✝
R : Type u
R' : Type ?u.298758
inst✝³ : Semiring R
inst✝² : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : PowerSeries S
⊢ ↑(ofPowerSeries ℤ S) (r • x) = r • ↑(ofPowerSeries ℤ S) x
ext
no goals
case coeff.h
R : Type u
R' : Type ?u.298758
inst✝³ : Semiring R
inst✝² : Ring R'
f g : PowerSeries R
f' g' : PowerSeries R'
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Module R S
r : R
x : PowerSeries S
x✝ : ℤ
⊢ HahnSeries.coeff (↑(ofPowerSeries ℤ S) (r • x)) x✝ = HahnSeries.coeff (r • ↑(ofPowerSeries ℤ S) x) x✝
simp [coeff_coe, coeff_smul, smul_ite]