k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(x /ᵒᶠ 0) x✝ = ↑x x✝
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
⊢ x /ᵒᶠ 0 = x
refine Finsupp.ext fun _ => ?_
no goals
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
x✝ : G
⊢ ↑(x /ᵒᶠ 0) x✝ = ↑x x✝
simp only [AddMonoidAlgebra.divOf_apply, zero_add]