Theorems · Definition · commutative algebra

Polynomial.sylvester

{R : Type u_1} → [inst : Semiring R] → Polynomial R → Polynomial R → (m n : ℕ) → Matrix (Fin (m + n)) (Fin (m + n)) R

The Sylvester matrix of two polynomials f and g of degrees m and n respectively is a (m+n) × (m+n) 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. Note that the natural definition would be a Matrix (Fin (m + n)) (Fin m ⊕ Fin n) R but we prefer having this as a square matrix to take determinants later on.

Defined in

Mathlib.RingTheory.Polynomial.Resultant.Basic

Cited by

18 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring