det_vandermonde_id_eq_superFactorial

English

The determinant of Vandermonde on the nodes 0,1,...,n equals n.superFactorial.

Русский

Определитель матрицы Вандермонде для узлов 0,1,...,n равен n.superFactorial.

LaTeX

$$$\\det(\\operatorname{vandermonde}(\\mathrm{fun}\\ i:\\mathrm{Fin}(n+1) \\mapsto i)) = n.\\mathrm{superFactorial}$$$

Lean4

theorem det_vandermonde_id_eq_superFactorial (n : ℕ) :
    (vandermonde fun i : Fin (n + 1) ↦ (i : R)).det = n.superFactorial := by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [Nat.superFactorial, det_vandermonde, Fin.prod_univ_succAbove _ 0]
    push_cast
    congr
    · simp only [Fin.val_zero, Nat.cast_zero, sub_zero]
      norm_cast
      simp [Fin.prod_univ_eq_prod_range (fun i ↦ (↑i + 1)) (n + 1)]
    · rw [det_vandermonde] at hn
      simp [hn]

Похожие утверждения