feat(linear_algebra/vandermonde): add lemmas about det equals zero (#14695)
feat(linear_algebra/vandermonde): add lemmas about det equals zero (#14695)

Adding two lemmas about when the determinant is zero.
I shortened the first with the help of some code I found in `ring_theory/trace.lean`, lemma `det_trace_matrix_ne_zero'`.



Co-authored-by: Bart Michels <5339f3b1a4d0a0b4ec47e106feffc833d7f72251@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib