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

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