English
Let p_i be polynomials with deg(p_i) = i and p_i monic. The matrix A with A_{i j} = coeff_i(p_j) has determinant 1.
Русский
Пусть p_i — полиномы с deg(p_i) = i и p_i монические. Матрица A с A_{i j} = коэффициент_i(p_j) имеет детерминант, равный 1.
LaTeX
$$$\det\big( A \big) = 1 \quad\text{where } A_{i j} = [p_j]_i,\; \deg(p_j)=j,\; p_j\text{ монитик}$$$
Lean4
theorem det_matrixOfPolynomials {n : ℕ} (p : Fin n → R[X]) (h_deg : ∀ i, (p i).natDegree = i)
(h_monic : ∀ i, Monic <| p i) : (Matrix.of (fun (i j : Fin n) => (p j).coeff i)).det = 1 :=
by
rw [Matrix.det_of_upperTriangular (Matrix.matrixOfPolynomials_blockTriangular p (fun i ↦ Nat.le_of_eq (h_deg i)))]
convert prod_const_one with x _
rw [Matrix.of_apply, ← h_deg, coeff_natDegree, (h_monic x).leadingCoeff]
