case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
r : R
x : HahnSeries Γ R
x✝ : Γ
⊢ coeff (↑(single 0) r * x) x✝ = coeff (r • x) x✝
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
r : R
x : HahnSeries Γ R
⊢ ↑(single 0) r * x = r • x
ext
no goals
case coeff.h
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
r : R
x : HahnSeries Γ R
x✝ : Γ
⊢ coeff (↑(single 0) r * x) x✝ = coeff (r • x) x✝
exact single_zero_mul_coeff