English
The determinant of Vandermonde with nodes 0,1,...,n equals n.superFactorial (up to canonical casting).
Русский
Определитель матрицы Вандермонде для узлов 0,1,...,n равен n.superFactorial (с необходимым приведением типа).
LaTeX
$$$\\det(\\operatorname{vandermonde}(i \\mapsto i)) = n.\\mathrm{superFactorial}.$$$
Lean4
/-- Note: the "obvious" statement `(piCongrLeft P e) f b = f (e.symm b)` doesn't typecheck: the
LHS would have type `P b` while the RHS would have type `P (e (e.symm b))`. For that reason,
we have to explicitly substitute along `e (e.symm b) = b` in the statement of this lemma. -/
theorem piCongrLeft_apply (f : ∀ a, P (e a)) (b : β) : (piCongrLeft P e) f b = e.apply_symm_apply b ▸ f (e.symm b) :=
rfl
