English
Definition: For polynomials f and g, the Sylvester matrix Sylvester(f,g;m,n) is the (n+m)×(n+m) matrix whose entries are built from the coefficients of f and g in a canonical block arrangement.
Русский
Определение: для многочленов f и g матрица Сильвестра Sylvester(f,g;m,n) есть (n+m)×(n+m) матрица, чьи элементы строятся из коэффициентов f и g в канонической блочной записи.
LaTeX
$$$\\text{Sylvester}(f,g;m,n) \\in \\mathrm{Mat}_{(n+m)\\times(n+m)}(R)$$$
Lean4
/-- The Sylvester matrix of two polynomials `f` and `g` of degrees `m` and `n` respectively is a
`(n+m) × (n+m)` matrix with the coefficients of `f` and `g` arranged in a specific way. Here, `m`
and `n` are free variables, not necessarily equal to the actual degrees of the polynomials `f` and
`g`. -/
def sylvester (f g : R[X]) (m n : ℕ) : Matrix (Fin (n + m)) (Fin (n + m)) R :=
.of fun i j ↦
j.addCases (fun j₁ ↦ if (i : ℕ) ∈ Set.Icc (j₁ : ℕ) (j₁ + m) then f.coeff (i - j₁) else 0)
(fun j₁ ↦ if (i : ℕ) ∈ Set.Icc (j₁ : ℕ) (j₁ + n) then g.coeff (i - j₁) else 0)
