Commit 2023-11-08 11:24 9efe273d

View on Github →

feat: superFactorial_dvd_vandermonde_det (#6893)

Estimated changes

Modified Mathlib/Data/Nat/Factorial/SuperFactorial.lean

added theorem Nat.prod_range_succ_factorial

added theorem Nat.superFactorial_dvd_vandermonde_det

Modified Mathlib/LinearAlgebra/Matrix/Block.lean

added theorem Matrix.det_matrixOfPolynomials

added theorem Matrix.matrixOfPolynomials_blockTriangular

Modified Mathlib/LinearAlgebra/Vandermonde.lean

added theorem Matrix.det_eval_matrixOfPolynomials_eq_det_vandermonde

added theorem Matrix.eval_matrixOfPolynomials_eq_vandermonde_mul_matrixOfPolynomials

Modified docs/references.bib