matrixOfPolynomials_blockTriangular

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

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