Theorem: ENat.tsum_mul (Matroid/ForMathlib/ENatTopology.lean)

State before:
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
c : ℕ∞
⊢ (∑' (a : α), f a) * c = ∑' (a : α), f a * c
Tactic:
simp_rw [ENat.tsum_eq_iSup_sum, ENat.iSup_mul, Finset.sum_mul]
State after:
no goals