simp [v, pair, pair', Weight.sum, Finset.mul_sum, Finset.sum_sub_distrib, sub_mul, mul_assoc]
n d : ℕ
inst✝ : NeZero d
w : Weight n d
a : ↑(testvecs n d)
⊢ pair' w (v a) = ↑d * ↑(Weight.sum w) - (↑n + 1) * ↑(pair w ↑a)
no goals