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