Commit 2025-08-29 09:38 a0072886

View on Github →

chore(Data): move results about the Vandermonde matrix to LinearAlgebra (#29095) These have nothing to do with data structures.

Estimated changes

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

deleted theorem Nat.det_vandermonde_id_eq_superFactorial

deleted theorem Nat.superFactorial_dvd_vandermonde_det

Modified Mathlib/LinearAlgebra/Vandermonde.lean

added theorem Matrix.det_vandermonde_id_eq_superFactorial

added theorem Matrix.superFactorial_dvd_vandermonde_det