English
Given polynomials p_i with deg p_i ≤ i, the matrix of coefficients A with A_{i j} = coeff_i(p_j) is block triangular with respect to the natural order.
Русский
Даны полиномы p_i с deg p_i ≤ i. Матрица коэффициентов A с A_{i j} = коэффициент_i(p_j) является блочно-верхнетреугольной по естественному порядку.
LaTeX
$$$\text{BlockTriangular}(A, \mathrm{id})$ where $A_{i j} = [p_j]_i$ and $\deg(p_j) \le j$$$
Lean4
theorem matrixOfPolynomials_blockTriangular {R} [Semiring R] {n : ℕ} (p : Fin n → R[X])
(h_deg : ∀ i, (p i).natDegree ≤ i) : Matrix.BlockTriangular (Matrix.of (fun (i j : Fin n) => (p j).coeff i)) id :=
fun _ j h => by exact coeff_eq_zero_of_natDegree_lt <| Nat.lt_of_le_of_lt (h_deg j) h