no goals
Γ : Type u_2
R✝ : Type ?u.2750260
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : Semiring R✝
α : Type u_3
R : Type u_1
inst✝ : Ring R
s t : SummableFamily Γ R α
⊢ hsum (s - t) = hsum s - hsum t
rw [← lsum_apply, LinearMap.map_sub, lsum_apply, lsum_apply]