super factorial and vandermonde determinant

Stream: PR reviews

[Moritz Firsching]

I have formalized

theorem superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) :
   ↑(superFactorial n) ∣ (Matrix.vandermonde v).det

and thought this would make a nice addition to Mathlib.LinearAlgebra.Vandermonde (perhaps with R instead of ℤ) and I started to make pull requests to add the super factorial and related things, as well as theorems in Vandermonde.
Reviews/Feedback for those would be most welcome: #6768, #6806, #6812, #6827

[Moritz Firsching]

Here is the draft pull request with the result about the super factorial dividing the vandermonde determinant: #6893.
This is not quite ready for review, but the prerequisites (#6768, #6806, #6812, #6827) are ready for review. (Thanks @Eric Wieser and @Alex J. Best for already taking a look at some of them...)

In #6893 I still need to replace my custom polynomial_descFactorial, with pochhammer, but I pochhammer is more like polynomidal_ascFactorial....

[Yaël Dillies]

Why not keep it as descPochhammer?

[Moritz Firsching]

Yeah, that's what I meant, I will use descPochammer, once we have it.
By now I have pending pull request for the Monic and natDegree properties needed for descPochhammer:
#6927 and #6929 , both of them depends on the rename and adding descPochhammer, i.e. #6918 and #6917

I tried to make all of the pull requests small, so that they would be easier to review...

[Moritz Firsching]

By now most parts for

theorem superFactorial_dvd_vandermonde_det {n : ℕ} (v : Fin (n + 1) → ℤ) :
   ↑(Nat.superFactorial n) ∣ (Matrix.vandermonde v).det

are ready, see #6893. There are a few lemmas around properties of the matrix

Matrix.of (fun (i j : Fin n) => (p j).coeff i)

I'm not sure if they are of any relevance outside the proof or not. I would appreciate if someone could take a look.