simp only [Weight.sum, Finset.mul_sum]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ Weight.sum (k • w) = k * Weight.sum w
n d : ℕ
inst✝ : NeZero d
w : Weight n d
k : ℕ
⊢ ∑ j : Fin (Nat.succ n), (k • w) j = ∑ i : Fin (Nat.succ n), k * w i