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

Commit
3 years ago
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 <97157072+bartmichels@users.noreply.github.com>
Author
Parents
Loading