rw [mul_comm k, ← Finset.sum_mul]
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), ↑a x * k = k * d
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ (∑ i : Fin (Nat.succ n), ↑a i) * k = d * k