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