no goals
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
i j : Fin n
⊢ ((vandermonde v)ᵀ ⬝ vandermonde v) i j = ∑ k : Fin n, v k ^ (↑i + ↑j)
simp only [vandermonde_apply, Matrix.mul_apply, Matrix.transpose_apply, pow_add]