simp only [pair, smul_apply, one_apply, mul_one]
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ pair (k • 1) ↑a = k * d
n d : ℕ
inst✝ : NeZero d
a : ↑(testvecs n d)
k : ℕ
⊢ ∑ x : Fin (Nat.succ n), ↑a x * k = k * d