mathlib

252cb024 - feat(linear_algebra/vandermonde): `vandermonde v` multiplied by its transpose (#8776)

feat(linear_algebra/vandermonde): `vandermonde v` multiplied by its transpose (#8776) Two not very exciting lemmas about multiplying a Vandermonde matrix by its transpose (one for each side). I don't know if they are really useful, so I could also just inline them in #8777.